diff options
| author |  Jason Gross <jgross@mit.edu> | 2018-02-13 17:24:12 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2018-02-13 17:24:12 -0500 |
| commit | 70f1d999ff030d20d10f23bcbf95f37216e182c9 (patch) | |
| tree | 016cb1532ca7f14ecec171af9ea4e2739b4d8621 /test-suite/coq-makefile/timing | |
| parent | 4f65dfb13d8bb395abf4aa405cae9ed529302a06 (diff) | |
Fix issue with spurious timing test failures
When none of the numbers get over 100, the width of the table was
different.
See https://github.com/coq/coq/pull/6736#issuecomment-365386802
Diffstat (limited to 'test-suite/coq-makefile/timing')
| -rwxr-xr-x | test-suite/coq-makefile/timing/run.sh | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/coq-makefile/timing/run.sh b/test-suite/coq-makefile/timing/run.sh index 2439d3f37..dfcc31569 100755 --- a/test-suite/coq-makefile/timing/run.sh +++ b/test-suite/coq-makefile/timing/run.sh @@ -74,7 +74,7 @@ echo for ext in "" .desired; do for file in A.v.timing.diff; do - cat ${file}${ext} | sed s"/${INFINITY}/${INFINITY_REPLACEMENT}/g" | sed s":|\s*N/A\s*$:| ${INFINITY_REPLACEMENT}:g" | sed s'/[0-9]*\.[0-9]*//g' | sed s'/0//g' | sed s'/ */ /g' | sed s'/ *$//g' | sed s'/+/-/g' | sort > ${file}${ext}.processed + cat ${file}${ext} | sed s"/${INFINITY}/${INFINITY_REPLACEMENT}/g" | sed s":|\s*N/A\s*$:| ${INFINITY_REPLACEMENT}:g" | sed s'/[0-9]*\.[0-9]*//g' | sed s'/0//g' | sed s'/^-*$/------/g' | sed s'/ */ /g' | sed s'/ *$//g' | sed s'/+/-/g' | sort > ${file}${ext}.processed done done for file in A.v.timing.diff; do |