diff options
| author | yoni206 <yoni206@users.noreply.github.com> | 2020-05-30 21:17:59 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-05-30 21:17:59 -0700 |
| commit | b771d6bd159aed8dc5449871dd0607c31bd47081 (patch) | |
| tree | 13498e46f0dc9c09d7fff40ac97163f577b97c5a | |
| parent | ba659fb1b8bc2f110616ec113892f63f210a5ebb (diff) | |
update example in README to use ctest. (#4540)
An example for restricting timeout in tests uses the old `make regress0` instead of the new `ctest -L regress0`
| -rw-r--r-- | test/regress/README.md | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test/regress/README.md b/test/regress/README.md index 28ccfb96b..0dc1d4eb8 100644 --- a/test/regress/README.md +++ b/test/regress/README.md @@ -12,7 +12,7 @@ By default, each invocation of CVC4 is done with a 10 minute timeout. To use a different timeout, set the `TEST_TIMEOUT` environment variable: ``` -TEST_TIMEOUT=0.5 make regress0 +TEST_TIMEOUT=0.5 ctest -L regress0 ``` This runs regression tests from level 0 with a 0.5 second timeout. |