summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorMaxim Kuvyrkov <maxim.kuvyrkov@linaro.org>2019-01-19 13:59:00 +0000
committerMaxim Kuvyrkov <maxim.kuvyrkov@linaro.org>2019-01-20 07:40:15 +0000
commita61032cab5def612c864bb10c5e35d4f44d708db (patch)
tree80bd55eabc04a50fd6488101a6bad003b870afe1
parent00370c419fe52c9a21c29b9832d78863d5fe5bdd (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.sh7
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
)
}