configure: support --with-docs=no

Since we promise --with-foo=no is equivalent to --without-foo

diff --git a/configure b/configure
index 1e17b4649f8ebf97f77a5e0b2d0d43e1e9c6f490..c415568cb2ab12d876c78b054a48851da50a5999 100755 (executable)
--- a/configure
+++ b/configure
@@ -187,6 +187,12 @@ for option; do
        BASHCOMPLETIONDIR="${option#*=}"
     elif [ "${option%%=*}" = '--zshcompletiondir' ] ; then
        ZSHCOMLETIONDIR="${option#*=}"
+    elif [ "${option%%=*}" = '--with-docs' ]; then
+       if [ "${option#*=}" = 'no' ]; then
+           WITH_DOCS=0
+       else
+           WITH_DOCS=1
+       fi
     elif [ "${option}" = '--without-docs' ] ; then
        WITH_DOCS=0
     elif [ "${option%%=*}" = '--with-emacs' ]; then