From 8794dbd18c61109298b827146bcd2b370f5798bd Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Fri, 17 Nov 2017 15:30:14 -0500
Subject: Have the coq_makefile timing test-suite print more

This should help debug things like
https://github.com/coq/coq/issues/5675#issuecomment-345324924 if they
ever show up again.
---
 test-suite/coq-makefile/timing/run.sh | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/test-suite/coq-makefile/timing/run.sh b/test-suite/coq-makefile/timing/run.sh
index 7e0baaa8f2..2428da7316 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
 
-- 
cgit v1.2.3