diff options
| -rwxr-xr-x | test-suite/check | 7 |
1 files changed, 2 insertions, 5 deletions
diff --git a/test-suite/check b/test-suite/check index 1c7822d104..5bc034aec7 100755 --- a/test-suite/check +++ b/test-suite/check @@ -9,7 +9,7 @@ else fi if [ "$1" = -byte ]; then - command="../bin/coqtop.byte -q -batch -load-vernac-source" + command="../bin/coqtop.byte -no-vm -q -batch -load-vernac-source" else command="../bin/coqtop -q -batch -load-vernac-source" fi @@ -99,7 +99,7 @@ test_parser() { foutput=`dirname $f`/`basename $f .v`.out echo "parse_file 1 \"$f\"" | ../bin/parser > $tmpoutput 2>&1 perl -ne 'if(/Starting.*Parser Loop/){$printit = 1};print if $printit' \ - $tmpoutput | grep -i error > /dev/null + $tmpoutput 2>&1 | grep -i error > /dev/null if [ $? = 0 ] ; then echo "Error! (unexpected output)" else @@ -124,6 +124,3 @@ test_parser parser pourcentage=`expr 100 \* $nbtestsok / $nbtests` echo echo "$nbtestsok tests passed over $nbtests, i.e. $pourcentage %" - - - |