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