summaryrefslogtreecommitdiff
path: root/configure.ac
diff options
context:
space:
mode:
authorChristopher L. Conway <christopherleeconway@gmail.com>2010-08-24 17:09:40 +0000
committerChristopher L. Conway <christopherleeconway@gmail.com>2010-08-24 17:09:40 +0000
commitd8c37e4d1cbe1c99b1b5fc250085419b9de4e513 (patch)
treecc2b037e1df5f0e7fa8254692729bdb26e823428 /configure.ac
parent314e777887f32c8cf656dbc56f370da6dd0bf76e (diff)
Making GMP default, CLN opt-in with --with-cln
Diffstat (limited to 'configure.ac')
-rw-r--r--configure.ac20
1 files changed, 13 insertions, 7 deletions
diff --git a/configure.ac b/configure.ac
index c65dea9dc..939ad53a2 100644
--- a/configure.ac
+++ b/configure.ac
@@ -172,6 +172,9 @@ AC_PROG_INSTALL
# determine whether to use CLN or GMP.
# we do this here so it can affect the build directory
+# [chris 8/24/2010] The user *must* specify --with-cln to get CLN
+# (and, thus, opt in to the GPL dependency).
+
cvc4_use_gmp=0
cvc4_use_cln=0
@@ -179,24 +182,27 @@ AC_ARG_WITH(
[cln],
AS_HELP_STRING(
[--with-cln],
- [use CLN instead of GMP (default, if CLN found)]
+ [use CLN instead of GMP]
),
- [if test "$withval" = no; then
- cvc4_use_gmp=1
- else
+ [if test "$withval" != no; then
cvc4_use_cln=1
fi
]
)
+# [chris 8/24/2010] --with-gmp has no practical effect, since GMP is
+# the default. Could be useful if other options are added later.
+
AC_ARG_WITH(
[gmp],
AS_HELP_STRING(
[--with-gmp],
- [use GMP instead of CLN]
+ [use GMP instead of CLN (default)]
),
[if test "$withval" = no; then
- cvc4_use_cln=1
+ if test $cvc4_use_cln = 0; then
+ AC_MSG_ERROR([You must use either CLN and GMP. Please pick one.])
+ fi
else
cvc4_use_gmp=1
fi
@@ -208,7 +214,7 @@ if test $cvc4_use_cln = 1 && test $cvc4_use_gmp = 1; then
AC_MSG_ERROR([You cannot use both CLN and GMP. Please pick one.])
fi
-if test $cvc4_use_cln = 1 || test $cvc4_use_cln = 0 -a $cvc4_use_gmp = 0; then
+if test $cvc4_use_cln = 1; then
# [mdeters] The PKG_CHECK_MODULES macro isn't customizable and doesn't fail
# gracefully. You can only specify it once for a given library name. That
# is, even on separate if/else branches, you can't put
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback