diff --git a/configure.sh b/configure.sh index b2a8e3cff..413652ddc 100755 --- a/configure.sh +++ b/configure.sh @@ -5,9 +5,9 @@ echo "Configuring the repository for development..." -SKIP_MAP_DOWNLOAD=$SKIP_MAP_DOWNLOAD -SKIP_GENERATE_SYMBOLS=$SKIP_GENERATE_SYMBOLS -SKIP_GENERATE_DRULES=$SKIP_GENERATE_DRULES +SKIP_MAP_DOWNLOAD="${SKIP_MAP_DOWNLOAD:-}" +SKIP_GENERATE_SYMBOLS="${SKIP_GENERATE_SYMBOLS:-}" +SKIP_GENERATE_DRULES="${SKIP_GENERATE_DRULES:-}" DRULES_NOT_GENERATED= SYMBOLS_NOT_GENERATED=