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 /src | |
| 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 'src')
| -rw-r--r-- | src/CMakeLists.txt | 8 |
1 files changed, 2 insertions, 6 deletions
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index c7192dcf7..13ab74d4b 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -1284,9 +1284,7 @@ set(KINDS_FILES add_subdirectory(base) add_subdirectory(context) add_subdirectory(expr) -if (NOT BUILD_LIB_ONLY) - add_subdirectory(parser) -endif() +add_subdirectory(parser) add_subdirectory(theory) add_subdirectory(util) @@ -1359,9 +1357,7 @@ target_link_libraries(cvc5 PRIVATE GMP) # target_link_libraries(...) with object libraries for cmake versions <= 3.12. # Thus, we can only visit main as soon as all dependencies for cvc5 are set up. -if (NOT BUILD_LIB_ONLY) - add_subdirectory(main) -endif() +add_subdirectory(main) #-----------------------------------------------------------------------------# # Install public API headers |