diff options
author | Jason Gross <jgross@mit.edu> | 2017-11-17 15:30:14 -0500 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2017-11-17 15:30:14 -0500 |
commit | 8794dbd18c61109298b827146bcd2b370f5798bd (patch) | |
tree | 0ed0553493c1eb48dd3cd375ddd7bc5162846770 /test-suite/coq-makefile/timing/run.sh | |
parent | edf1a8f36f75861b822081b3825357e122b6937d (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/timing/run.sh')
-rwxr-xr-x | test-suite/coq-makefile/timing/run.sh | 10 |
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 |