diff options
Diffstat (limited to 'Makefile.config.in')
| -rw-r--r-- | Makefile.config.in | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/Makefile.config.in b/Makefile.config.in index 7d3c05f6..d9572f7d 100644 --- a/Makefile.config.in +++ b/Makefile.config.in @@ -35,6 +35,7 @@ STP_LDFLAGS := @STP_LDFLAGS@ ENABLE_METASMT := @ENABLE_METASMT@ METASMT_ROOT := @METASMT_ROOT@ +METASMT_DEFAULT_BACKEND := @METASMT_DEFAULT_BACKEND@ ENABLE_Z3 := @ENABLE_Z3@ Z3_CFLAGS := @Z3_CFLAGS@ @@ -50,6 +51,8 @@ HAVE_SELINUX := @HAVE_SELINUX@ HAVE_TCMALLOC := @HAVE_TCMALLOC@ TCMALLOC_LIB := @TCMALLOC_LIB@ +HAVE_ZLIB := @HAVE_ZLIB@ + RUNTIME_ENABLE_OPTIMIZED := @RUNTIME_ENABLE_OPTIMIZED@ RUNTIME_DISABLE_ASSERTIONS := @RUNTIME_DISABLE_ASSERTIONS@ RUNTIME_DEBUG_SYMBOLS := @RUNTIME_DEBUG_SYMBOLS@ |