diff options
| author | Gereon Kremer <nafur42@gmail.com> | 2021-09-28 20:10:45 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-09-29 03:10:45 +0000 |
| commit | a42b56e46f579b57eb0a3f49d1195881670375e7 (patch) | |
| tree | 5a9f033cf8492768ed47c4ca6d0832f8bb43e6ea /test | |
| parent | 1c1add20d0842ea347fffb19bb3ad90eee665a3b (diff) | |
remove stuff (#7258)
This PR removes the BUILD_LIB_ONLY cmake option, and the associated --lib-only configure script option.
If you only want the library, just run make cvc5 instead of make.
Diffstat (limited to 'test')
| -rw-r--r-- | test/CMakeLists.txt | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/test/CMakeLists.txt b/test/CMakeLists.txt index ac1848994..d3ff709ca 100644 --- a/test/CMakeLists.txt +++ b/test/CMakeLists.txt @@ -35,9 +35,7 @@ add_custom_target(check #-----------------------------------------------------------------------------# # Add subdirectories -if (NOT BUILD_LIB_ONLY) - add_subdirectory(regress) -endif() +add_subdirectory(regress) add_subdirectory(api EXCLUDE_FROM_ALL) if(ENABLE_UNIT_TESTING) |