1 files changed, 13 insertions, 0 deletions
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=""