diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2016-01-26 17:18:24 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2016-01-26 17:18:24 +0100 |
commit | ad20f9ab9a6f4d9e080b27571fa411aa68a53907 (patch) | |
tree | 182f2c6cb72c2d450149c0a4f82463a2a6179663 /debian/patches/0002-Remove-test-4366-too-picky-on-the-timeout.patch | |
parent | bb08c29807439697fa7c2045000dd3e17a9428b1 (diff) |
8.5
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.patch | 30 |
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. |