diff options
| -rwxr-xr-x | configure.gnu | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/configure.gnu b/configure.gnu index 037d6ca6fb..46cc494fd6 100755 --- a/configure.gnu +++ b/configure.gnu @@ -65,6 +65,12 @@ EOM opts="$opts $arg" shift ;; + --prefix) + shift + arg="-Dprefix=$1" + opts="$opts $arg" + shift + ;; --cache-file=*) shift # Just ignore it. ;; |