diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-08-09 11:43:00 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-08-09 11:43:00 -0700 |
| commit | 5052848f548aefd50cca9550b750eb537eee258c (patch) | |
| tree | 7352898ebb68f9cb9cfe3ed1db39b16919a81ac8 /test/regress/README.md | |
| parent | 91d85704313de6be9fd382833f5cedd39e24a6fa (diff) | |
Fix documentation of regression tests (#2290)
Diffstat (limited to 'test/regress/README.md')
| -rw-r--r-- | test/regress/README.md | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/test/regress/README.md b/test/regress/README.md index 772332c3e..e1ac79976 100644 --- a/test/regress/README.md +++ b/test/regress/README.md @@ -22,10 +22,10 @@ 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.5s make regress0 +TEST_TIMEOUT=0.5 make regress0 ``` -This runs regression tests from level 0 with a 0,5 second timeout. +This runs regression tests from level 0 with a 0.5 second timeout. ## Adding New Regressions |