diff options
Diffstat (limited to 'test')
| -rwxr-xr-x | test/ocaml/run_tests.sh | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/test/ocaml/run_tests.sh b/test/ocaml/run_tests.sh index 40bd6af9..370048a0 100755 --- a/test/ocaml/run_tests.sh +++ b/test/ocaml/run_tests.sh @@ -74,7 +74,7 @@ cd $DIR for i in `ls -d */`; do cd $DIR/$i; - if $SAILDIR/sail -o out -ocaml_trace ../prelude.sail `ls *.sail` 1> /dev/null; + if $SAILDIR/sail -no_warn -o out -ocaml_trace ../prelude.sail `ls *.sail` 1> /dev/null; then ./out > result 2> /dev/null; if diff expect result; @@ -98,7 +98,7 @@ cd $DIR for i in `ls -d */`; do cd $DIR/$i; - if $SAILDIR/sail -is test.isail ../prelude.sail `ls *.sail` 1> /dev/null; + if $SAILDIR/sail -no_warn -is test.isail ../prelude.sail `ls *.sail` 1> /dev/null; then if diff expect result; then |