diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2018-09-10 09:30:35 -0700 |
---|---|---|
committer | Mathias Preiner <mathias.preiner@gmail.com> | 2018-09-22 16:30:59 -0700 |
commit | 562858328faaa68b0579de3f54738d7f5ce7e26a (patch) | |
tree | 371733be1f6cbfb75a96fe5b59c3df7d8c992cec /configure.sh | |
parent | 48a1e5fd59363e125c51cfb13f134ab2e80e9274 (diff) |
cmake: configure.sh wrapper: Configurable build directory
Diffstat (limited to 'configure.sh')
-rwxr-xr-x | configure.sh | 13 |
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="" |