From: yoni206 <yoni206@users.noreply.github.com>
Date: Sun, 31 May 2020 04:17:59 +0000 (-0700)
Subject: update example in README to use ctest. (#4540)
X-Git-Tag: cvc5-1.0.0~3280
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b771d6bd159aed8dc5449871dd0607c31bd47081;p=cvc5.git

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`
---

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.