aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/coq-makefile
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2017-11-17 15:30:14 -0500
committerGravatar Jason Gross <jgross@mit.edu>2017-11-17 15:30:14 -0500
commit8794dbd18c61109298b827146bcd2b370f5798bd (patch)
tree0ed0553493c1eb48dd3cd375ddd7bc5162846770 /test-suite/coq-makefile
parentedf1a8f36f75861b822081b3825357e122b6937d (diff)
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.
Diffstat (limited to 'test-suite/coq-makefile')
-rwxr-xr-xtest-suite/coq-makefile/timing/run.sh10
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