diff options
| author |  Benjamin Barenblat <bbaren@debian.org> | 2019-02-05 12:11:16 -0500 |
|---|---|---|
| committer | Benjamin Barenblat <bbaren@debian.org> | 2019-02-05 12:30:49 -0500 |
| commit | c40a76c5acdba3dc141cbeaf250ca394ae29ee20 (patch) | |
| tree | 1aa8ae7259b7f684d9c32484ae58de0922a07c44 /debian/patches/test-suite-success-Nsatz.v-comment-out-Ceva.patch | |
| parent | fe4de3af9df2d093394d89f702993d49ce41d70a (diff) | |
Consolidate patches to disable tests that are too big or too slow
Consolidate the several patches that disable tests that time out on
MIPS or use too much RAM/time on the buildds.
Diffstat (limited to 'debian/patches/test-suite-success-Nsatz.v-comment-out-Ceva.patch')
| -rw-r--r-- | debian/patches/test-suite-success-Nsatz.v-comment-out-Ceva.patch | 29 |
1 files changed, 0 insertions, 29 deletions
diff --git a/debian/patches/test-suite-success-Nsatz.v-comment-out-Ceva.patch b/debian/patches/test-suite-success-Nsatz.v-comment-out-Ceva.patch deleted file mode 100644 index 2cf6af5c..00000000 --- a/debian/patches/test-suite-success-Nsatz.v-comment-out-Ceva.patch +++ /dev/null @@ -1,29 +0,0 @@ -From: Stephane Glondu <steph@glondu.net> -Date: Sun, 15 Jan 2012 12:34:19 +0100 -Subject: test-suite/success/Nsatz.v: comment out Ceva - -This lemma uses too much memory for many buildds... ---- - test-suite/success/Nsatz.v | 2 ++ - 1 file changed, 2 insertions(+) - -diff --git a/test-suite/success/Nsatz.v b/test-suite/success/Nsatz.v -index e38affd..040169e 100644 ---- a/test-suite/success/Nsatz.v -+++ b/test-suite/success/Nsatz.v -@@ -462,6 +462,7 @@ idtac "chords". - (*Finished transaction in 4. secs (3.959398u,0.s)*) - Qed. - -+(* - Lemma Ceva: forall A B C D E F M:point, - collinear M A D -> collinear M B E -> collinear M C F -> - collinear B C D -> collinear E A C -> collinear F A B -> -@@ -473,6 +474,7 @@ idtac "Ceva". - Time nsatz. - (*Finished transaction in 105. secs (104.121171u,0.474928s)*) - Qed. -+*) - - Lemma bissectrices: forall A B C M:point, - equaltangente C A M M A B -> |