summaryrefslogtreecommitdiff
path: root/src/base/configuration_private.h
diff options
context:
space:
mode:
authorMathias Preiner <mathias.preiner@gmail.com>2018-05-21 17:54:09 -0700
committerGitHub <noreply@github.com>2018-05-21 17:54:09 -0700
commitdf02923c0f0c6589098064d0dfac0de1ef27537c (patch)
treecc94822345c80712fa8b6dfaa058c0bcb3d5a0a4 /src/base/configuration_private.h
parente50e09efa679c2d0c835cbf794a7b0743347552a (diff)
Add SymFPU licensing information. (#1952)
Diffstat (limited to 'src/base/configuration_private.h')
-rw-r--r--src/base/configuration_private.h6
1 files changed, 6 insertions, 0 deletions
diff --git a/src/base/configuration_private.h b/src/base/configuration_private.h
index cf9117100..018c7f800 100644
--- a/src/base/configuration_private.h
+++ b/src/base/configuration_private.h
@@ -138,6 +138,12 @@ namespace CVC4 {
# define IS_READLINE_BUILD false
#endif /* HAVE_LIBREADLINE */
+#ifdef CVC4_USE_SYMFPU
+#define IS_SYMFPU_BUILD true
+#else /* HAVE_SYMFPU_HEADERS */
+#define IS_SYMFPU_BUILD false
+#endif /* HAVE_SYMFPU_HEADERS */
+
#if CVC4_GPL_DEPS
# define IS_GPL_BUILD true
#else /* CVC4_GPL_DEPS */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback