diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-04-16 21:08:38 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-04-16 21:08:38 -0700 |
| commit | 8b9baa66ad6ffc9e323b83bc967992439a7d9bfa (patch) | |
| tree | bdb58c5a3249dc5f573284c306d529e4e3bd8067 /config | |
| parent | 8a079f9b982a502995da8e535a4b4487489af0d2 (diff) | |
Add timeout (option) to regression script (#1786)
This commit adds the option to run regressions with a timeout using the
`TEST_TIMEOUT` environment variable. The default timeout is set to 10
minutes. This should make it less likely that our nightly builds hang
and makes it easier to sort out slow tests.
Default timeout tested with regression level 2 on a debug build with
proofs.
Diffstat (limited to 'config')
0 files changed, 0 insertions, 0 deletions