From 16c89c1007c37bccbd86acf4d406c0c3d268cfdc Mon Sep 17 00:00:00 2001
From: David Gekeler <git@davidgekeler.eu>
Date: Sun, 25 May 2025 15:58:25 +0200
Subject: [PATCH] Add skip generate_symbols option

Signed-off-by: David Gekeler <git@davidgekeler.eu>
---
 configure.sh | 13 ++++++++++---
 1 file changed, 10 insertions(+), 3 deletions(-)

diff --git a/configure.sh b/configure.sh
index 3160d6872..3bad7e384 100755
--- a/configure.sh
+++ b/configure.sh
@@ -4,10 +4,11 @@
 #
 
 SKIP_MAP_DOWNLOAD=false
+SKIP_GENERATE_SYMBOLS=false
 
 ############################# PROCESS OPTIONS ################################
 
-TEMP=$(getopt -o s --long skip-map-download \
+TEMP=$(getopt -o ms --long skip-map-download,skip-generate-symbols \
               -n 'configure' -- "$@")
 
 if [ $? != 0 ] ; then echo "Terminating..." >&2 ; exit 1 ; fi
@@ -16,7 +17,8 @@ eval set -- "$TEMP"
 
 while true; do
   case "$1" in
-    -s | --skip-map-download ) SKIP_MAP_DOWNLOAD=true; shift ;;
+    -m | --skip-map-download ) SKIP_MAP_DOWNLOAD=true; shift ;;
+    -s | --skip-generate-symbols ) SKIP_GENERATE_SYMBOLS=true; shift ;;
     * ) break ;;
   esac
 done
@@ -46,6 +48,11 @@ else
   echo "Skipping world map download..."
 fi
 
-bash ./tools/unix/generate_symbols.sh
+if [ "$SKIP_GENERATE_SYMBOLS" = false ]; then
+  echo "Generating symbols..."
+  bash ./tools/unix/generate_symbols.sh
+else
+  echo "Skipping generate symbols..."
+fi
 
 echo "The repository is configured for development."