diff options
| author | coqbot-app[bot] | 2020-10-10 09:02:29 +0000 |
|---|---|---|
| committer | GitHub | 2020-10-10 09:02:29 +0000 |
| commit | 03d55f990bb7a2c4f5c1fefa408b94a8a93e8d05 (patch) | |
| tree | 17de76aba63396c735e6f49cd1a613ea557cb23f /dev/bench/gitlab.sh | |
| parent | 516a7009b08c443a74ef7f3175fff1337e71b668 (diff) | |
| parent | c7294a49205fed15ca413f65a1e5d3fbd14646e7 (diff) | |
Merge PR #13164: [bench] Dump the vo size difference.
Reviewed-by: SkySkimmer
Diffstat (limited to 'dev/bench/gitlab.sh')
| -rwxr-xr-x | dev/bench/gitlab.sh | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/dev/bench/gitlab.sh b/dev/bench/gitlab.sh index 7625e4e7f7..41f204385f 100755 --- a/dev/bench/gitlab.sh +++ b/dev/bench/gitlab.sh @@ -428,6 +428,9 @@ for coq_opam_package in $sorted_coq_opam_packages; do new_base_path=$new_ocaml_switch/.opam-switch/build/$coq_opam_package.dev*/ old_base_path=$old_ocaml_switch/.opam-switch/build/$coq_opam_package.dev*/ for vo in `cd $new_opam_root/$new_base_path/; find -name '*.vo'`; do + if [ -e $old_opam_root/$old_base_path/$vo ]; then + echo "$coq_opam_package/$vo $(stat -c%s $old_opam_root/$old_base_path/$vo) $(stat -c%s $new_opam_root/$new_base_path/$vo)" >> "$log_dir/vosize.log" + fi if [ -e $old_opam_root/$old_base_path/${vo%%o}.timing -a \ -e $new_opam_root/$new_base_path/${vo%%o}.timing ]; then mkdir -p $working_dir/html/$coq_opam_package/`dirname $vo`/ |