From c7294a49205fed15ca413f65a1e5d3fbd14646e7 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 26 Aug 2020 17:41:04 +0200
Subject: [bench] Dump the vo size difference.

---
 dev/bench/gitlab.sh | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'dev/bench/gitlab.sh')

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`/
-- 
cgit v1.2.3