Make configure{,.gnu} ignore --cache-file option

diff --git a/configure b/configure
index 868e45411185251f7ef8c26efc67408ff4b2b04c..30af30d30fafc8c1881c5558f51fd8a4a67e43ea 100755 (executable)
--- a/configure
+++ b/configure
@@ -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 868e45411185251f7ef8c26efc67408ff4b2b04c..30af30d30fafc8c1881c5558f51fd8a4a67e43ea 100755 (executable)
--- 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