Merge PR #6178: Have the coq_makefile timing test-suite print more

1 files changed, 10 insertions, 0 deletions

diff --git a/test-suite/coq-makefile/timing/run.sh b/test-suite/coq-makefile/timing/run.sh
index 7e0baaa8f..2428da731 100755
--- a/test-suite/coq-makefile/timing/run.sh
+++ b/test-suite/coq-makefile/timing/run.sh
@@ -41,6 +41,9 @@ for ext in "" .desired; do
     done
 done
 for file in time-of-build-before.log time-of-build-after.log time-of-build-both.log; do
+    echo "cat $file"
+    cat "$file"
+    echo
     diff -u $file.desired.processed $file.processed || exit $?
 done
 
@@ -56,6 +59,13 @@ make all TIMING=after -j2 || exit $?
 
 find ../per-file-before/ -name "*.before-timing" -exec 'cp' '{}' './' ';'
 make all.timing.diff -j2 || exit $?
+echo "cat A.v.before-timing"
+cat A.v.before-timing
+echo
+echo "cat A.v.after-timing"
+cat A.v.after-timing
+echo
+echo "cat A.v.timing.diff"
 cat A.v.timing.diff
 echo