[bench] Only upload some files

We will now also record a listing of all files that we could have
uploaded, in case we want to know what's available to upload in the
future.

1 files changed, 14 insertions, 0 deletions

diff --git a/dev/bench/gitlab.sh b/dev/bench/gitlab.sh
index fe17769d99..7625e4e7f7 100755
--- a/dev/bench/gitlab.sh
+++ b/dev/bench/gitlab.sh
@@ -114,6 +114,15 @@ else
     exit 1
 fi
 
+if which du > /dev/null; then
+    :
+else
+    echo > /dev/stderr
+    echo "ERROR: \"du\" program is not available." > /dev/stderr
+    echo > /dev/stderr
+    exit 1
+fi
+
 if [ ! -e "$working_dir" ]; then
     echo > /dev/stderr
     echo "ERROR: \"$working_dir\" does not exist." > /dev/stderr
@@ -430,6 +439,11 @@ for coq_opam_package in $sorted_coq_opam_packages; do
     done
 done
 
+# Since we do not upload all files, store a list of the files
+# available so that if we at some point want to tweak which files we
+# upload, we'll know which ones are available for upload
+du -ha "$working_dir" > "$working_dir/files.listing"
+
 # The following directories in $working_dir are no longer used:
 #
 # - coq, opam.OLD, opam.NEW