diff options
| author | Pierre-Marie Pédrot | 2020-08-26 17:41:04 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-10-09 12:06:03 +0200 |
| commit | c7294a49205fed15ca413f65a1e5d3fbd14646e7 (patch) | |
| tree | beef1665a48adfb8310708926f1e447a6ca43a6d /dev/bench | |
| parent | cc3ef68a475140bf7d3ca7a2fd3bc593508eb42c (diff) | |
[bench] Dump the vo size difference.
Diffstat (limited to 'dev/bench')
| -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`/ |