diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2016-09-13 12:55:00 +0200 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2016-09-13 12:58:07 +0200 |
| commit | 881d38c4c64fb3f3c346d5fbea15999fd6110ae9 (patch) | |
| tree | e2ba5b29430bcc8c351a5f872c7e89da72b857d1 /test-suite/Makefile | |
| parent | 61ad52acc91cc954e39006864f253c0f08b1ba80 (diff) | |
test-suite/output-modulo-time made more robust
Diffstat (limited to 'test-suite/Makefile')
| -rw-r--r-- | test-suite/Makefile | 12 |
1 files changed, 9 insertions, 3 deletions
diff --git a/test-suite/Makefile b/test-suite/Makefile index a3050bfcc..1dfbb29ff 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -304,10 +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 's/\s*[0-9]*\.[0-9]\+\s*//g' \ - | sed 's/\s*0\.\s*//g' \ + | sed -e 's/\s*[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 's/\s*[0-9]*\.[0-9]\+\s*//g' $*.out | sed 's/\s*0\.\s*//g' > $$tmpexpected; \ + sed -e 's/\s*[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; \ diff -b -u $$tmpexpected $$tmpoutput 2>&1; R=$$?; times; \ if [ $$R = 0 ]; then \ echo $(log_success); \ |