1 files changed, 30 insertions, 0 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
new file mode 100644
index 00000000..e71306ce
--- /dev/null
+++ b/debian/patches/0002-Remove-test-4366-too-picky-on-the-timeout.patch
@@ -0,0 +1,30 @@
+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.