#! /bin/sh /usr/share/dpatch/dpatch-run
## check.dpatch by Samuel Mimram <smimram@debian.org>
##
## All lines beginning with `## DP:' are a description of the patch.
## DP: Suppress warnings from tests outputs.

@DPATCH@
diff -urNad coq~/test-suite/check coq/test-suite/check
--- coq~/test-suite/check	2008-07-25 15:36:31.000000000 +0200
+++ coq/test-suite/check	2008-07-25 15:36:31.000000000 +0200
@@ -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
 	if [ $? = 0 ]; then