diff options
author | Matthieu Sozeau <mattam@mattam.org> | 2016-09-28 17:58:06 +0200 |
---|---|---|
committer | Matthieu Sozeau <mattam@mattam.org> | 2016-09-29 15:22:41 +0200 |
commit | 5348a615a484e379896deac8a6944af1f92b2d4c (patch) | |
tree | 9c97e883cd338b41568a1d4c759f280c9fbea55e | |
parent | 83435e2c02cfe450eddde50eb92ed2b501f25dfc (diff) |
test-suite: fix sed on OS X, does not handle +
-rw-r--r-- | test-suite/Makefile | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index 1dfbb29ff..a40ea80ae 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -304,16 +304,16 @@ $(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]\+\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]\+\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' \ - $*.out > $$tmpexpected; \ + $*.out > $$tmpexpected; \ diff -b -u $$tmpexpected $$tmpoutput 2>&1; R=$$?; times; \ if [ $$R = 0 ]; then \ echo $(log_success); \ |