summaryrefslogtreecommitdiff
path: root/INSTALL.md
diff options
context:
space:
mode:
Diffstat (limited to 'INSTALL.md')
-rw-r--r--INSTALL.md4
1 files changed, 2 insertions, 2 deletions
diff --git a/INSTALL.md b/INSTALL.md
index 9e0c9dfc4..98cef2061 100644
--- a/INSTALL.md
+++ b/INSTALL.md
@@ -297,7 +297,7 @@ All custom test targets build and run a preconfigured set of tests.
- `make check [-jN] [ARGS=-jN]`
The default build-and-test target for CVC4, builds and runs all examples,
- all system and unit tests, and regression tests from levels 0 and 1.
+ all system and unit tests, and regression tests from levels 0 to 2.
- `make systemtests [-jN] [ARGS=-jN]`
Build and run all system tests.
@@ -306,7 +306,7 @@ All custom test targets build and run a preconfigured set of tests.
Build and run all unit tests.
- `make regress [-jN] [ARGS=-jN]`
- Build and run regression tests from levels 0 and 1.
+ Build and run regression tests from levels 0 to 2.
- `make runexamples [-jN] [ARGS=-jN]`
Build and run all examples.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback