diff options
Diffstat (limited to 'Makefile.config.in')
| -rw-r--r-- | Makefile.config.in | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/Makefile.config.in b/Makefile.config.in index 9e04711b..35f7bcfe 100644 --- a/Makefile.config.in +++ b/Makefile.config.in @@ -36,6 +36,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@ |