projects / cvc5.git / commitdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | patch | inline | side by side (parent: 516862b)
Fix output of --show-config for readline. (#1159)
authorMathias Preiner <mathias.preiner@gmail.com>
Fri, 29 Sep 2017 03:32:36 +0000 (20:32 -0700)
committerAndres Noetzli <andres.noetzli@gmail.com>
Fri, 29 Sep 2017 03:32:36 +0000 (20:32 -0700)
cvc4 --show-config reported the wrong configuration for readline since
HAVE_LIBREADLINE is set to 0 or 1 but was checked with #ifdef.

src/base/configuration_private.h patch | blob | history

diff --git a/src/base/configuration_private.h b/src/base/configuration_private.h
index 6d9201dde8537d4f5b33c972b63f451ee4ffb521..472113c2e76095c968f47e6ae6695b175d48b6da 100644 (file)
--- a/src/base/configuration_private.h
+++ b/src/base/configuration_private.h
@@ -126,7 +126,7 @@ namespace CVC4 {
 #define IS_LFSC_BUILD false
 #endif /* CVC4_USE_LFSC */
 
-#ifdef HAVE_LIBREADLINE
+#if HAVE_LIBREADLINE
 #  define IS_READLINE_BUILD true
 #else /* HAVE_LIBREADLINE */
 #  define IS_READLINE_BUILD false