summaryrefslogtreecommitdiff
path: root/test-suite/coq-makefile/timing/run.sh
diff options
context:
space:
mode:
authorGravatar Benjamin Barenblat <bbaren@debian.org>2019-02-02 19:29:23 -0500
committerGravatar Benjamin Barenblat <bbaren@debian.org>2019-02-02 19:29:23 -0500
commit9ebf44d84754adc5b64fcf612c6816c02c80462d (patch)
treebf5e06a28488e0e06a2f2011ff0d110e2e02f8fc /test-suite/coq-makefile/timing/run.sh
parent9043add656177eeac1491a73d2f3ab92bec0013c (diff)
Imported Upstream version 8.9.0upstream/8.9.0upstream
Diffstat (limited to 'test-suite/coq-makefile/timing/run.sh')
-rwxr-xr-xtest-suite/coq-makefile/timing/run.sh27
1 files changed, 12 insertions, 15 deletions
diff --git a/test-suite/coq-makefile/timing/run.sh b/test-suite/coq-makefile/timing/run.sh
index f0e036ee..78a3f7c6 100755
--- a/test-suite/coq-makefile/timing/run.sh
+++ b/test-suite/coq-makefile/timing/run.sh
@@ -62,16 +62,14 @@ TO_SED_IN_PER_LINE=(
-e s'/ */ /g' # Sometimes 0 will show up as 0m00.s, sometimes it'll end up being more like 0m00.001s; we must strip out the spaces that result from left-aligning numbers of different widths based on how many digits Coq's [-time] gives
)
-for ext in "" .desired; do
- for file in time-of-build-before.log time-of-build-after.log time-of-build-both.log; do
- cat ${file}${ext} | grep -v 'warning: undefined variable' | sed "${TO_SED_IN_BOTH[@]}" "${TO_SED_IN_PER_FILE[@]}" > ${file}${ext}.processed
- 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 $?
+ for ext in "" .desired; do
+ grep -v 'warning: undefined variable' < ${file}${ext} | sed "${TO_SED_IN_BOTH[@]}" "${TO_SED_IN_PER_FILE[@]}" > ${file}${ext}.processed
+ done
+ echo "cat $file"
+ cat "$file"
+ echo
+ diff -u $file.desired.processed $file.processed || exit $?
done
cd ../per-file-before
@@ -96,13 +94,12 @@ echo "cat A.v.timing.diff"
cat A.v.timing.diff
echo
+file=A.v.timing.diff
+
for ext in "" .desired; do
- for file in A.v.timing.diff; do
- cat ${file}${ext} | sed "${TO_SED_IN_BOTH[@]}" "${TO_SED_IN_PER_LINE[@]}" | sort > ${file}${ext}.processed
- done
-done
-for file in A.v.timing.diff; do
- diff -u $file.desired.processed $file.processed || exit $?
+ sed "${TO_SED_IN_BOTH[@]}" "${TO_SED_IN_PER_LINE[@]}" < "${file}${ext}" | sort > "${file}${ext}.processed"
done
+diff -u "$file.desired.processed" "$file.processed" || exit $?
+
exit 0