diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2016-09-30 12:58:03 +0200 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2016-09-30 12:58:03 +0200 |
commit | a7a3e5b4d6df64b9bee42a86cd018c19ac6b01c0 (patch) | |
tree | 938a412d43a2e14c42ac42cb197f1654f6f839f9 /test-suite/Makefile | |
parent | 7543449792d417a92092b692986d62b622b78ffc (diff) | |
parent | c4c7aa6d7b14a6d76c287b97d487abe055406577 (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/Makefile | 4 |
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' \ |