diff options
Diffstat (limited to 'configure.sh')
| -rwxr-xr-x | configure.sh | 7 |
1 files changed, 0 insertions, 7 deletions
diff --git a/configure.sh b/configure.sh index ae9b275aa..bd95e38ed 100755 --- a/configure.sh +++ b/configure.sh @@ -34,7 +34,6 @@ The following flags enable optional features (disable with --no-<option name>). --valgrind Valgrind instrumentation --debug-context-mm use the debug context memory manager --statistics include statistics - --replay turn on the replay feature --assertions turn on assertions --tracing include tracing code --dumping include dumping code @@ -130,7 +129,6 @@ lfsc=default muzzle=default optimized=default proofs=default -replay=default shared=default static_binary=default statistics=default @@ -248,9 +246,6 @@ do --proofs) proofs=ON;; --no-proofs) proofs=OFF;; - --replay) replay=ON;; - --no-replay) replay=OFF;; - --static) shared=OFF; static_binary=ON;; --no-static) shared=ON;; @@ -387,8 +382,6 @@ cmake_opts="" && cmake_opts="$cmake_opts -DENABLE_OPTIMIZED=$optimized" [ $proofs != default ] \ && cmake_opts="$cmake_opts -DENABLE_PROOFS=$proofs" -[ $replay != default ] \ - && cmake_opts="$cmake_opts -DENABLE_REPLAY=$replay" [ $shared != default ] \ && cmake_opts="$cmake_opts -DENABLE_SHARED=$shared" [ $static_binary != default ] \ |