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 /test/regress/Makefile.am | |
| 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 'test/regress/Makefile.am')
| -rw-r--r-- | test/regress/Makefile.am | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/test/regress/Makefile.am b/test/regress/Makefile.am index 19cbbae4a..ba1442c69 100644 --- a/test/regress/Makefile.am +++ b/test/regress/Makefile.am @@ -57,5 +57,5 @@ EXTRA_DIST = \ regress0/tptp/Axioms/SYN000_0.ax \ Makefile.levels \ Makefile.tests \ - run_regression.py \ - README.md
\ No newline at end of file + run_regression.py \ + README.md |