diff options
Diffstat (limited to 'debian/patches/no-complexity-test.dpatch')
| -rwxr-xr-x | debian/patches/no-complexity-test.dpatch | 21 |
1 files changed, 0 insertions, 21 deletions
diff --git a/debian/patches/no-complexity-test.dpatch b/debian/patches/no-complexity-test.dpatch deleted file mode 100755 index 5f9bff67..00000000 --- a/debian/patches/no-complexity-test.dpatch +++ /dev/null @@ -1,21 +0,0 @@ -#! /bin/sh /usr/share/dpatch/dpatch-run -## no-complexity-test.dpatch by Julien Cristau <julien.cristau@ens-lyon.org> -## -## All lines beginning with `## DP:' are a description of the patch. -## DP: Don't run complexity tests, they are far too fragile. - -@DPATCH@ -diff -urNad coq~/test-suite/check coq/test-suite/check ---- coq~/test-suite/check 2008-07-25 15:13:00.000000000 +0200 -+++ coq/test-suite/check 2008-07-25 15:33:55.000000000 +0200 -@@ -250,8 +250,8 @@ - test_interactive interactive - echo "Micromega tests" - test_success micromega --echo "Complexity tests" --test_complexity complexity -+echo "Skipping complexity tests" -+#test_complexity complexity - echo "Module tests" - $coqtop -compile modules/Nat - $coqtop -compile modules/plik |