diff --git a/tools/unix/build_omim.sh b/tools/unix/build_omim.sh index efb9479dd..62541416d 100755 --- a/tools/unix/build_omim.sh +++ b/tools/unix/build_omim.sh @@ -2,6 +2,10 @@ set -euo pipefail +SKIP_MAP_DOWNLOAD=$SKIP_MAP_DOWNLOAD +SKIP_GENERATE_SYMBOLS=$SKIP_GENERATE_SYMBOLS +SKIP_GENERATE_DRULES=$SKIP_GENERATE_DRULES + OPT_DEBUG= OPT_RELEASE= OPT_RELEASEDEBUGINFO= @@ -76,8 +80,10 @@ OMIM_PATH="$(cd "${OMIM_PATH:-$(dirname "$0")/../..}"; pwd)" if [ "$OPT_TARGET" == "desktop" ]; then ./configure.sh -else +elif [ -z "$SKIP_MAP_DOWNLOAD$SKIP_GENERATE_SYMBOLS$SKIP_GENERATE_DRULES" ] SKIP_MAP_DOWNLOAD=1 SKIP_GENERATE_SYMBOLS=1 SKIP_GENERATE_DRULES=1 ./configure.sh +else + ./configure.sh fi DEVTOOLSET_PATH=/opt/rh/devtoolset-7