Add timeout (option) to regression script (#1786)
authorAndres Noetzli <andres.noetzli@gmail.com>
Tue, 17 Apr 2018 04:08:38 +0000 (21:08 -0700)
committerGitHub <noreply@github.com>
Tue, 17 Apr 2018 04:08:38 +0000 (21:08 -0700)
commit8b9baa66ad6ffc9e323b83bc967992439a7d9bfa
treebdb58c5a3249dc5f573284c306d529e4e3bd8067
parent8a079f9b982a502995da8e535a4b4487489af0d2
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.
test/regress/Makefile.am
test/regress/README.md
test/regress/run_regression.py