--- test-suite/check 2009-01-05 09:01:04.000000000 -0500 +++ test-suite/check 2009-04-08 08:05:08.000000000 -0400 @@ -52,7 +52,7 @@ nbtests=`expr $nbtests + 1` printf " "$f"..." tmpoutput=`mktemp /tmp/coqcheck.XXXXXX` - $command $f 2>&1 | grep -v "Welcome to Coq" | grep -v "Skipping rcfile loading" > $tmpoutput + $command $f 2>&1 | grep -v "Welcome to Coq" | grep -v "Skipping rcfile loading" | grep -v "some rule has been masked" > $tmpoutput foutput=`dirname $f`/`basename $f .v`.out diff $tmpoutput $foutput > /dev/null 2>&1 if [ $? = 0 ]; then