about summary refs log tree commit diff homepage
path: root/scripts
diff options
context:
space:
mode:
Diffstat (limited to 'scripts')
-rw-r--r--scripts/build/p-klee.inc2
-rw-r--r--scripts/build/v-klee.inc1
2 files changed, 3 insertions, 0 deletions
diff --git a/scripts/build/p-klee.inc b/scripts/build/p-klee.inc
index 8479a2ca..a1520f83 100644
--- a/scripts/build/p-klee.inc
+++ b/scripts/build/p-klee.inc
@@ -138,6 +138,8 @@ fi
   else
     CMAKE_ARGUMENTS+=("-DCMAKE_BUILD_TYPE=Debug")
   fi
+
+  CMAKE_ARGUMENTS+=("-DKLEE_RUNTIME_BUILD_TYPE=${KLEE_RUNTIME_BUILD}")
   
 # TODO: We should support Ninja too
 # Configure KLEE
diff --git a/scripts/build/v-klee.inc b/scripts/build/v-klee.inc
index 62fdf9dd..5f7d9fca 100644
--- a/scripts/build/v-klee.inc
+++ b/scripts/build/v-klee.inc
@@ -1,6 +1,7 @@
 # Build information for KLEE
 required_variables_klee=(
   "COVERAGE"
+  "KLEE_RUNTIME_BUILD"
   "USE_TCMALLOC"
   "USE_LIBCXX"
 )