diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-04-03 22:39:42 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-04-03 22:39:42 +0200 |
| commit | ef9beacfe10383fcb8a42f92f754bc4dcb391a67 (patch) | |
| tree | d60f693b1e37090b657b8923dfc8203c8d1a83df | |
| parent | f29f8f80c8ad94576c7a36f3f638866c208338a0 (diff) | |
| parent | d768015a3f7667525fd3daa8d5a83122b9d8dcaa (diff) | |
Merge PR #7154: Update coq_makefile timing test
| -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 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 |