diff options
Diffstat (limited to 'test-suite')
| -rwxr-xr-x | test-suite/check | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/test-suite/check b/test-suite/check index 4ccc1dc57..65c4197eb 100755 --- a/test-suite/check +++ b/test-suite/check @@ -84,14 +84,14 @@ test_parser() { printf " "$f"..." tmpoutput=`mktemp /tmp/coqcheck.XXXXXX` foutput=`dirname $f`/`basename $f .v`.out - echo "parse_file 1 \"$f\"" | ../bin/parser -v7 > $tmpoutput 2>&1 + echo "parse_file 1 \"$f\"" | ../bin/parser > $tmpoutput 2>&1 perl -ne 'if(/Starting.*Parser Loop/){$printit = 1};print if $printit' \ - $tmpoutput | diff - $foutput > /dev/null + $tmpoutput | grep -i error > /dev/null if [ $? = 0 ] ; then + echo "Error! (unexpected output)" + else echo "Ok" nbtestsok=`expr $nbtestsok + 1` - else - echo "Error! (unexpected output)" fi done fi |