diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-06-16 17:13:45 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-06-16 17:13:45 +0200 |
| commit | 52ab54dc6734319203442f36de4d7ddd4fd999b9 (patch) | |
| tree | f86178325dd95e71252c034676d22df7fd1d0bde | |
| parent | db522eb68496f56c11d43cb269c4d14943f334af (diff) | |
| parent | f70f12b56e44abd9df4ad6941ee4941a761302fa (diff) | |
Merge PR#804: Increase the time limit on 4366.v to make gitlab work better.
| -rw-r--r-- | test-suite/bugs/closed/4366.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/bugs/closed/4366.v b/test-suite/bugs/closed/4366.v index 6a5e9a402..403c2d202 100644 --- a/test-suite/bugs/closed/4366.v +++ b/test-suite/bugs/closed/4366.v @@ -10,6 +10,6 @@ end. Goal True. Proof. pose (v := stupid 24). -Timeout 2 vm_compute in v. +Timeout 4 vm_compute in v. exact I. Qed. |