diff options
author | Maxim Kuvyrkov <maxim.kuvyrkov@linaro.org> | 2019-01-19 13:59:00 +0000 |
---|---|---|
committer | Maxim Kuvyrkov <maxim.kuvyrkov@linaro.org> | 2019-01-20 07:40:15 +0000 |
commit | a61032cab5def612c864bb10c5e35d4f44d708db (patch) | |
tree | 80bd55eabc04a50fd6488101a6bad003b870afe1 | |
parent | 00370c419fe52c9a21c29b9832d78863d5fe5bdd (diff) |
jenkins-helpers.sh: Fix fresh_dir and use it in git_clean
Find races with "rm -rf" and complains about missing files
and directories that were just deleted. Ignore find's exit
status and stderr.
Change-Id: Ie79b9ef56e4932a694cdee16b31384efd99f1c1f
-rw-r--r-- | jenkins-helpers.sh | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/jenkins-helpers.sh b/jenkins-helpers.sh index 658bd4dc..b63fa150 100644 --- a/jenkins-helpers.sh +++ b/jenkins-helpers.sh @@ -40,7 +40,7 @@ fresh_dir () done done - find "$dir" "${find_opts[@]}" -print0 | xargs -0 rm -rf + find "$dir" "${find_opts[@]}" -delete ) } @@ -928,10 +928,9 @@ print_kernel_target () git_clean () { ( set -euf -o pipefail - local dir="$1" - cd "$dir" - find -maxdepth 1 ! -name .git ! -name . -print0 | xargs -0 -r rm -rf + fresh_dir "$1" "$1/.git/*" + git -C "$1" reset --hard ) } |