diff options
Diffstat (limited to 'debian/patches/check.dpatch')
| -rwxr-xr-x | debian/patches/check.dpatch | 19 |
1 files changed, 0 insertions, 19 deletions
diff --git a/debian/patches/check.dpatch b/debian/patches/check.dpatch deleted file mode 100755 index d0cb3907..00000000 --- a/debian/patches/check.dpatch +++ /dev/null @@ -1,19 +0,0 @@ -#! /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 |