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 f92f453f..7d3c05f6 100644 --- a/Makefile.config.in +++ b/Makefile.config.in @@ -47,6 +47,9 @@ KLEE_UCLIBC_BCA := @KLEE_UCLIBC_BCA@ HAVE_SELINUX := @HAVE_SELINUX@ +HAVE_TCMALLOC := @HAVE_TCMALLOC@ +TCMALLOC_LIB := @TCMALLOC_LIB@ + RUNTIME_ENABLE_OPTIMIZED := @RUNTIME_ENABLE_OPTIMIZED@ RUNTIME_DISABLE_ASSERTIONS := @RUNTIME_DISABLE_ASSERTIONS@ RUNTIME_DEBUG_SYMBOLS := @RUNTIME_DEBUG_SYMBOLS@ |