diff options
Diffstat (limited to 'test-suite')
| -rwxr-xr-x | test-suite/check | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/check b/test-suite/check index aa6bef1ebc..3a10d0e163 100755 --- a/test-suite/check +++ b/test-suite/check @@ -82,7 +82,7 @@ test_parser() { printf " "$f"..." tmpoutput=`mktemp /tmp/coqcheck.XXXXXX` foutput=`dirname $f`/`basename $f .v`.out - echo "parse_file 1 \"$f\"" | ../bin/parser > $tmpoutput 2>&1 + echo "parse_file 1 \"$f\"" | ../bin/parser -v7 > $tmpoutput 2>&1 perl -ne 'if(/Starting.*Parser Loop/){$printit = 1};print if $printit' \ $tmpoutput | diff - $foutput > /dev/null if [ $? = 0 ] ; then |