aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2018-04-03 22:39:42 +0200
committerGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2018-04-03 22:39:42 +0200
commitef9beacfe10383fcb8a42f92f754bc4dcb391a67 (patch)
treed60f693b1e37090b657b8923dfc8203c8d1a83df
parentf29f8f80c8ad94576c7a36f3f638866c208338a0 (diff)
parentd768015a3f7667525fd3daa8d5a83122b9d8dcaa (diff)
Merge PR #7154: Update coq_makefile timing test
-rwxr-xr-xtest-suite/coq-makefile/timing/run.sh2
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 aa6b0a9a4..43c83e412 100755
--- a/test-suite/coq-makefile/timing/run.sh
+++ b/test-suite/coq-makefile/timing/run.sh
@@ -40,7 +40,7 @@ INFINITY_REPLACEMENT="+.%" # assume that if the before time is zero, we expected
TO_SED_IN_BOTH=(
-e s"/${INFINITY}/${INFINITY_REPLACEMENT}/g" # Whether or not something shows up as ∞ depends on whether a time registers as 0.s or as 0.001s, so we can't rely on this being consistent
- -e s":|\s*N/A\s*$:| ${INFINITY_REPLACEMENT}:g" # Whether or not something shows up as N/A depends on whether a time registers as 0.s or as 0.001s, so we can't rely on this being consistent
+ -e s':|\s*N/A\s*$:| '"${INFINITY_REPLACEMENT}"':g' # Whether or not something shows up as N/A depends on whether a time registers as 0.s or as 0.001s, so we can't rely on this being consistent
-e s'/ *$//g' # the number of trailing spaces depends on how many digits percentages end up being; since this varies across runs, we remove trailing spaces
-e s'/[0-9]*\.[0-9]*//g' # the precise timing numbers vary, so we strip them out
-e s'/^-*$/------/g' # When none of the numbers get over 100 (or 1000, in per-file), the width of the table is different, so we normalize the number of dashes for table separators