diff options
| -rwxr-xr-x | configure | 4 | ||||
| -rwxr-xr-x | configure.gnu | 4 |
2 files changed, 8 insertions, 0 deletions
@@ -46,6 +46,7 @@ It emulates the following GNU configure options (must be fully spelled out): --help --no-create --prefix=PREFIX + --cache-file (ignored) --quiet --silent --verbose @@ -64,6 +65,9 @@ EOM opts="$opts $arg" shift ;; + --cache-file=*) + shift # Just ignore it. + ;; --quiet|--silent) exec >/dev/null 2>&1 shift diff --git a/configure.gnu b/configure.gnu index 868e454111..30af30d30f 100755 --- a/configure.gnu +++ b/configure.gnu @@ -46,6 +46,7 @@ It emulates the following GNU configure options (must be fully spelled out): --help --no-create --prefix=PREFIX + --cache-file (ignored) --quiet --silent --verbose @@ -64,6 +65,9 @@ EOM opts="$opts $arg" shift ;; + --cache-file=*) + shift # Just ignore it. + ;; --quiet|--silent) exec >/dev/null 2>&1 shift |