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