diff options
| author | Gaëtan Gilbert | 2017-06-16 11:07:23 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2017-06-16 11:07:23 +0200 |
| commit | f70f12b56e44abd9df4ad6941ee4941a761302fa (patch) | |
| tree | eacb63c11cab82f8aea9bfb6413baf9d4234d73f | |
| parent | 1d3703be3ab41d016c776bb29d9f5eff0cdb401d (diff) | |
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 6a5e9a4023..403c2d2026 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. |