From 562858328faaa68b0579de3f54738d7f5ce7e26a Mon Sep 17 00:00:00 2001
From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Mon, 10 Sep 2018 09:30:35 -0700
Subject: [PATCH] cmake: configure.sh wrapper: Configurable build directory

---
 configure.sh | 13 +++++++++++++
 1 file changed, 13 insertions(+)

diff --git a/configure.sh b/configure.sh
index 468fa0f6b..0a4aa996f 100755
--- a/configure.sh
+++ b/configure.sh
@@ -14,6 +14,7 @@ Build types:
 
 General options;
   -h, --help               display this help and exit
+  --build-dir-prefix       prefix build directory with given prefix
   --best                   turn on dependences known to give best performance
   --gpl                    permit GPL dependences, if available
 
@@ -160,6 +161,7 @@ msg () {
 #--------------------------------------------------------------------------#
 
 builddir=default
+prefix=""
 
 #--------------------------------------------------------------------------#
 
@@ -224,6 +226,15 @@ do
     --best) best=ON;;
     --no-best) best=OFF;;
 
+    --build-dir-prefix)
+      shift
+      if [ $# -eq 0 ]
+      then
+        die "missing argument to --build-dir-prefix"
+      fi
+      prefix=$1
+      ;;
+
     --cadical) cadical=ON;;
     --no-cadical) cadical=OFF;;
 
@@ -383,6 +394,8 @@ do
   shift
 done
 
+builddir="$prefix$builddir"
+
 #--------------------------------------------------------------------------#
 
 cmake_opts=""
-- 
2.30.2