projects / cvc5.git / commitdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | patch | inline | side by side (parent: 64165da)
Remove documentation for --lib-only (#7648)
authorAlex Ozdemir <aozdemir@hmc.edu>
Wed, 17 Nov 2021 01:18:46 +0000 (17:18 -0800)
committerGitHub <noreply@github.com>
Wed, 17 Nov 2021 01:18:46 +0000 (01:18 +0000)
The feature was removed in #7258.

configure.sh patch | blob | history

diff --git a/configure.sh b/configure.sh
index 319af54c5ee4218a77f74868efbde7205f20e869..970df2e616851954198db7339503ec548146dfce 100755 (executable)
--- a/configure.sh
+++ b/configure.sh
@@ -67,10 +67,6 @@ Optional Path to Optional Packages:
   --glpk-dir=PATH          path to top level of GLPK installation
   --dep-path=PATH          path to a dependency installation dir
 
-Build limitations:
-  --lib-only               only build the library, but not the executable or
-                           the parser (default: off)
-
 CMake Options (Advanced)
   -DVAR=VALUE              manually add CMake options