diff options
author | Mathias Preiner <mathias.preiner@gmail.com> | 2020-04-27 13:42:28 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-04-27 13:42:28 -0700 |
commit | dc9b11c33d0f3283b82f2c87bfd7dd4c7126b0d0 (patch) | |
tree | 1bbb7fbbd1b8332f28fd23388917f0d3eb9d6d6c /INSTALL.md | |
parent | 8476f38b6a3288eebe50e12a2dc6b76a10b65aae (diff) |
Fix examples instructions in INSTALL.md. (#4397)
Diffstat (limited to 'INSTALL.md')
-rw-r--r-- | INSTALL.md | 30 |
1 files changed, 1 insertions, 29 deletions
diff --git a/INSTALL.md b/INSTALL.md index 17d31fe1a..9fc2b52c1 100644 --- a/INSTALL.md +++ b/INSTALL.md @@ -203,17 +203,7 @@ binding, please contact one of the project leaders. ## Building the Examples -The examples provided in directory `examples` are not built by default. - - make examples # build all examples - make runexamples # build and run all examples - make <example> # build examples/<subdir>/<example>.<ext> - ctest example/<subdir>/<example> # run test example/<subdir>/<example> - -All examples binaries are built into `<build_dir>/bin/examples`. - -See `examples/README` for more detailed information on what to find in the -`examples` directory. +See `examples/README.md` for instructions on how to build and run the examples. ## Testing CVC4 @@ -238,24 +228,6 @@ We have 4 categories of tests: - **unit tests** in directory `test/unit` (label: **unit**) -### Testing Examples - -For building instructions, see [Building the Examples](building-the-examples). - -We use prefix `example/` + `<subdir>/` + `<example>` (for `<example>` in -`example/<subdir>/`) as test target name. - - make bitvectors # build example/api/bitvectors.cpp - ctest -R bitvectors # run all tests that match '*bitvectors*' - # > runs example/api/bitvectors - # > example/api/bitvectors_and_arrays - # > ... - ctest -R bitvectors$ # run all tests that match '*bitvectors' - # > runs example/api/bitvectors - ctest -R example/api/bitvectors$ # run all tests that match '*example/api/bitvectors' - # > runs example/api/bitvectors - - ### Testing System Tests The system tests are not built by default. |