diff options
Diffstat (limited to 'Makefile.config.in')
| -rw-r--r-- | Makefile.config.in | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/Makefile.config.in b/Makefile.config.in index 452cc1a1..a6dcdcaa 100644 --- a/Makefile.config.in +++ b/Makefile.config.in @@ -29,6 +29,12 @@ PROJ_INSTALL_ROOT := @prefix@ STP_ROOT := @STP_ROOT@ +STP_NEEDS_BOOST := @STP_NEEDS_BOOST@ + +ifeq ($(STP_NEEDS_BOOST),1) + UPSTREAM_STP_LINK_FLAGS = @UPSTREAM_STP_LINK_FLAGS@ +endif + ENABLE_METASMT := @ENABLE_METASMT@ METASMT_ROOT := @METASMT_ROOT@ @@ -36,6 +42,8 @@ ENABLE_POSIX_RUNTIME := @ENABLE_POSIX_RUNTIME@ ENABLE_STPLOG := @ENABLE_STPLOG@ ENABLE_UCLIBC := @ENABLE_UCLIBC@ +KLEE_UCLIBC_BCA := @KLEE_UCLIBC_BCA@ + HAVE_SELINUX := @HAVE_SELINUX@ RUNTIME_ENABLE_OPTIMIZED := @RUNTIME_ENABLE_OPTIMIZED@ @@ -66,3 +74,4 @@ LDFLAGS := @LDFLAGS@ -g REQUIRES_RTTI := @REQUIRES_RTTI@ RUNTEST := @RUNTEST@ +TCLSH := @TCLSH@ |