aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/4366.v
diff options
context:
space:
mode:
authorGravatar Gaëtan Gilbert <gaetan.gilbert@ens-lyon.fr>2017-06-16 11:07:23 +0200
committerGravatar Gaëtan Gilbert <gaetan.gilbert@ens-lyon.fr>2017-06-16 11:07:23 +0200
commitf70f12b56e44abd9df4ad6941ee4941a761302fa (patch)
treeeacb63c11cab82f8aea9bfb6413baf9d4234d73f /test-suite/bugs/closed/4366.v
parent1d3703be3ab41d016c776bb29d9f5eff0cdb401d (diff)
Increase the time limit on 4366.v to make gitlab work better.
Diffstat (limited to 'test-suite/bugs/closed/4366.v')
-rw-r--r--test-suite/bugs/closed/4366.v2
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.