aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/Makefile
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2016-09-30 12:58:03 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2016-09-30 12:58:03 +0200
commita7a3e5b4d6df64b9bee42a86cd018c19ac6b01c0 (patch)
tree938a412d43a2e14c42ac42cb197f1654f6f839f9 /test-suite/Makefile
parent7543449792d417a92092b692986d62b622b78ffc (diff)
parentc4c7aa6d7b14a6d76c287b97d487abe055406577 (diff)
Merge remote-tracking branch 'github/pr/303' into v8.6
Was PR#303: LtacProf cutoff is for total percent, not time
Diffstat (limited to 'test-suite/Makefile')
-rw-r--r--test-suite/Makefile4
1 files changed, 2 insertions, 2 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile
index 9d7444d7a..efa0236c3 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -305,12 +305,12 @@ $(addsuffix .log,$(wildcard output-modulo-time/*.v)): %.v.log: %.v %.out
| grep -v "\[Loading ML file" \
| grep -v "Skipping rcfile loading" \
| grep -v "^<W>" \
- | sed -e 's/\s*[0-9]*\.[0-9][0-9]*\s*//g' \
+ | sed -e 's/\s*[-+0-9]*\.[0-9][0-9]*\s*//g' \
-e 's/\s*0\.\s*//g' \
-e 's/\s*[-+]nan\s*//g' \
-e 's/\s*[-+]inf\s*//g' \
> $$tmpoutput; \
- sed -e 's/\s*[0-9]*\.[0-9][0-9]*\s*//g' \
+ sed -e 's/\s*[-+0-9]*\.[0-9][0-9]*\s*//g' \
-e 's/\s*0\.\s*//g' \
-e 's/\s*[-+]nan\s*//g' \
-e 's/\s*[-+]inf\s*//g' \