From 9d32c2e21228db2c1892198ddb8e5a17cec7bddd Mon Sep 17 00:00:00 2001
From: Willy Scheibel <willy.scheibel@hpi.de>
Date: Thu, 2 Nov 2023 18:13:04 +0100
Subject: [PATCH] Review configure setup

---
 .gitignore |  1 +
 configure  | 21 +++++++++++++++++----
 2 files changed, 18 insertions(+), 4 deletions(-)

diff --git a/.gitignore b/.gitignore
index afdd4c70a..2d4146940 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,3 +1,4 @@
+*-build*
 build*
 *_build
 /install
diff --git a/configure b/configure
index ea46f1be6..652046fdd 100755
--- a/configure
+++ b/configure
@@ -1,6 +1,7 @@
 #!/bin/bash
 
 # Default options
+
 BUILD_DIR="build"
 CMAKE_GENERATOR="Unix Makefiles"
 BUILD_TYPE="Release"
@@ -99,8 +100,18 @@ do
     fi
 done
 
+if [ "$CMAKE_GENERATOR_OVERRIDE" != "" ]
+then
+  echo "Override CMAKE_GENERATOR to $CMAKE_GENERATOR_OVERRIDE"
+  CMAKE_GENERATOR="$CMAKE_GENERATOR_OVERRIDE"
+fi
+
+if [ -n "$BUILD_DIR_PREFIX" ]; then
+  BUILD_DIR="${BUILD_DIR_PREFIX}-${BUILD_DIR}"
+fi
+
 # Configure build
-echo "Configuring ..."
+echo "Configuring in \"$BUILD_DIR\""
 echo ""
 
 # Create build directory
@@ -110,8 +121,11 @@ then
 fi
 
 # Configure project
+
 PREVIOUS_DIR=$(pwd)
-cd $BUILD_DIR
+
+pushd $BUILD_DIR
+echo cmake -G "$CMAKE_GENERATOR" "-DCMAKE_BUILD_TYPE=$BUILD_TYPE" $CMAKE_OPTIONS "$PREVIOUS_DIR"
 cmake -G "$CMAKE_GENERATOR" "-DCMAKE_BUILD_TYPE=$BUILD_TYPE" $CMAKE_OPTIONS "$PREVIOUS_DIR"
 if [ $? == 0 ]
 then
@@ -123,5 +137,4 @@ else
     echo ""
     echo "Configuration failed.";
 fi
-
-cd "$PREVIOUS_DIR"
+popd