diff --git a/configure b/configure index 92d290aba24..ab5f4f6991b 100755 --- a/configure +++ b/configure @@ -558,6 +558,13 @@ while [ "$#" -gt 0 ]; do cmake) BUILD_WITH_CMAKE=yes ;; + redo) + if [ -f config.opt ]; then + if grep -e ^-cmake