summaryrefslogtreecommitdiff
path: root/debian/patches/0002-Remove-test-4366-too-picky-on-the-timeout.patch
diff options
context:
space:
mode:
Diffstat (limited to 'debian/patches/0002-Remove-test-4366-too-picky-on-the-timeout.patch')
-rw-r--r--debian/patches/0002-Remove-test-4366-too-picky-on-the-timeout.patch30
1 files changed, 0 insertions, 30 deletions
diff --git a/debian/patches/0002-Remove-test-4366-too-picky-on-the-timeout.patch b/debian/patches/0002-Remove-test-4366-too-picky-on-the-timeout.patch
deleted file mode 100644
index e71306ce..00000000
--- a/debian/patches/0002-Remove-test-4366-too-picky-on-the-timeout.patch
+++ /dev/null
@@ -1,30 +0,0 @@
-From: Enrico Tassi <gareuselesinge@debian.org>
-Date: Tue, 26 Jan 2016 16:58:25 +0100
-Subject: Remove test 4366 (too picky on the timeout)
-
----
- test-suite/bugs/closed/4366.v | 15 ---------------
- 1 file changed, 15 deletions(-)
- delete mode 100644 test-suite/bugs/closed/4366.v
-
-diff --git a/test-suite/bugs/closed/4366.v b/test-suite/bugs/closed/4366.v
-deleted file mode 100644
-index 6a5e9a4..0000000
---- a/test-suite/bugs/closed/4366.v
-+++ /dev/null
-@@ -1,15 +0,0 @@
--Fixpoint stupid (n : nat) : unit :=
--match n with
--| 0 => tt
--| S n =>
-- let () := stupid n in
-- let () := stupid n in
-- tt
--end.
--
--Goal True.
--Proof.
--pose (v := stupid 24).
--Timeout 2 vm_compute in v.
--exact I.
--Qed.