aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/coq-makefile
diff options
context:
space:
mode:
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