diff options
| author | Pierre-Marie Pédrot | 2020-09-04 11:50:19 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-09-04 11:50:19 +0200 |
| commit | 2000ba38718e72133b258b378b118a495acb6ffc (patch) | |
| tree | 6c382de402b4c46250ccdf914df8228570924979 /dev | |
| parent | e5a1aaa831a0aa93e6f986a011f129ec6b59af7a (diff) | |
| parent | f9eeec7101da55263b644164d1f096af232eb995 (diff) | |
Merge PR #12900: [bench] Also upload the raw timing files, etc
Ack-by: SkySkimmer
Reviewed-by: ppedrot
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/bench/gitlab-bench.yml | 5 | ||||
| -rwxr-xr-x | dev/bench/gitlab.sh | 14 |
2 files changed, 19 insertions, 0 deletions
diff --git a/dev/bench/gitlab-bench.yml b/dev/bench/gitlab-bench.yml index a2207081f4..4275e3d121 100644 --- a/dev/bench/gitlab-bench.yml +++ b/dev/bench/gitlab-bench.yml @@ -28,5 +28,10 @@ bench: paths: - _bench/html/**/*.v.html - _bench/logs + - _bench/files.listing + - _bench/opam.NEW/**/*.log + - _bench/opam.NEW/**/*.timing + - _bench/opam.OLD/**/*.log + - _bench/opam.OLD/**/*.timing when: always expire_in: 1 year 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 |