diff options
3 files changed, 48 insertions, 1 deletions
diff --git a/scripts/ b/scripts/
index 2a107ed..8104ba7 100755
--- a/scripts/
+++ b/scripts/
@@ -40,7 +40,6 @@ set -x
mkdir -p "$deps"
cd "$deps"
-rm -rf "$project" "$project"
cd "$project"
if [ -n "$branch" ]; then
diff --git a/scripts/ b/scripts/
new file mode 100755
index 0000000..11a5b72
--- /dev/null
+++ b/scripts/
@@ -0,0 +1,42 @@
+# Clean workspace.
+# This should be the first and last step of every jenkins build:
+# a) to make sure the workspace has no build artifacts from previous runs.
+# b) to reduce disk space lost to unused binaries; parallel and/or matrix
+# builds create numerous workspaces, blowing up disk usage.
+# Note that if a build fails, the last steps will not run, hence calling this
+# as last step cleans only in case there was no build failure, i.e. where we
+# don't need to keep anything anyway.
+# Assume $PWD is a git clone's root dir. Usually, that's also the jenkins
+# workspace root. Do not wipe subdir 'layer1-headers' as well as all dirs under
+# '$deps'. These are assumed to be git clones that do not need to be re-cloned
+# every time. Do a 'git clean' in each of them individually. If '$deps' is not
+# defined or the mentioned dirs do not exist, nothing special happens, so this
+# script can be safely run in any git clone in deeper subdirs of the workspace.
+set -ex
+# make sure no write protected cruft is in the way. A failed 'make distcheck'
+# has a habit of leaving a non-writable dir tree behind.
+chmod -R +w .
+# wipe all local modifications
+git checkout -f HEAD
+# wipe all unversioned leftovers, except deps gits.
+git clean -dxf -e "$deps" -e "layer1-headers"
+# leave the deps checkouts around, to not clone entire git history every time,
+# but clean each git of build artifacts.
+if [ -d "$deps" ]; then
+ for dep_dir in "$deps"/* ; do
+ git checkout -f HEAD
+ git -C "$dep_dir" clean -dxf
+ done
+if [ -d "layer1-headers" ]; then
+ git checkout -f HEAD
+ git -C "layer1-headers" clean -dxf
diff --git a/scripts/ b/scripts/
index 86da9a6..c256a6a 100755
--- a/scripts/
+++ b/scripts/
@@ -8,5 +8,11 @@ fi
cd $1
git fetch origin
+# Cleanup should already have happened during a global,
+# but in case the caller did not (want to) call that, let's also do cleanup in
+# the dep subdir separately:
git reset --hard origin/master
git rev-parse HEAD