summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGereon Kremer <nafur42@gmail.com>2021-10-05 09:45:08 -0700
committerGitHub <noreply@github.com>2021-10-05 09:45:08 -0700
commit35de43d011528e34f42363c1d201b10bf254d386 (patch)
tree81e61391d422caa83b9628cc0fc0e5bc119af69c
parent13f5ecf0f7d683c67ab9b6e0cd66777af1b0531b (diff)
Reformulate (#7305)
-rw-r--r--CMakeLists.txt6
1 files changed, 3 insertions, 3 deletions
diff --git a/CMakeLists.txt b/CMakeLists.txt
index aaad41e9f..8e5a9c7e7 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -697,11 +697,11 @@ else()
"\n"
"Note that this configuration is NOT built against any GPL'ed libraries, so"
"\n"
- "it is covered by the (modified) BSD license. This is, however, not the best"
+ "it is covered by the (modified) BSD license. To build against GPL'ed"
"\n"
- "performing configuration of cvc5. To build against GPL'ed libraries which"
+ "libraries which can improve cvc5's performance on arithmetic and bitvector"
"\n"
- "improve cvc5's performance, re-configure with '-DENABLE_GPL -DENABLE_BEST'."
+ "logics, re-configure with '-DENABLE_GPL -DENABLE_BEST'."
)
endif()
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback