diff options
Diffstat (limited to 'configure.sh')
| -rwxr-xr-x | configure.sh | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/configure.sh b/configure.sh index d7e807c65..2057dd512 100755 --- a/configure.sh +++ b/configure.sh @@ -366,8 +366,6 @@ cmake_opts="" && cmake_opts="$cmake_opts -DENABLE_MUZZLE=$muzzle" [ $optimized != default ] \ && cmake_opts="$cmake_opts -DENABLE_OPTIMIZED=$optimized" -[ $portfolio != default ] \ - && cmake_opts="$cmake_opts -DENABLE_PORTFOLIO=$portfolio" [ $proofs != default ] \ && cmake_opts="$cmake_opts -DENABLE_PROOFS=$proofs" [ $replay != default ] \ |