diff options
Diffstat (limited to 'test-suite/coq-makefile/timing/run.sh')
| -rwxr-xr-x | test-suite/coq-makefile/timing/run.sh | 27 |
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 |