diff options
author | Mathias Preiner <mathias.preiner@gmail.com> | 2018-05-21 17:54:09 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-05-21 17:54:09 -0700 |
commit | df02923c0f0c6589098064d0dfac0de1ef27537c (patch) | |
tree | cc94822345c80712fa8b6dfaa058c0bcb3d5a0a4 /src/base/configuration_private.h | |
parent | e50e09efa679c2d0c835cbf794a7b0743347552a (diff) |
Add SymFPU licensing information. (#1952)
Diffstat (limited to 'src/base/configuration_private.h')
-rw-r--r-- | src/base/configuration_private.h | 6 |
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 */ |