diff --git a/autogen.sh b/autogen.sh index 80d7a305f..fa8cce072 100755 --- a/autogen.sh +++ b/autogen.sh @@ -12,7 +12,7 @@ set -e # try to pull submodules if we are in a git repo # might fail if git is not installed (how did you even checkout the # repo in the first place?) -if test -d '.git'; then +if test -d '.git' && [ -z "$SKIP_SUBMODULES" ] ; then printf 'git repository detected, updating submodule... ' git submodule update --init > /dev/null printf 'done\n' diff --git a/build-infer.sh b/build-infer.sh index 0c86bc2d3..def0d763f 100755 --- a/build-infer.sh +++ b/build-infer.sh @@ -135,7 +135,11 @@ install_opam_deps echo "preparing build... " if [ ! -f .release ]; then - ./autogen.sh > /dev/null + if [ "$BUILD_CLANG" = "no" ]; then + SKIP_SUBMODULES=true ./autogen.sh > /dev/null + else + ./autogen.sh > /dev/null + fi fi if [ "$BUILD_CLANG" = "no" ]; then