[PATCH 2/3] configure: support --with-docs=no

[David Bremner]

Since we promise --with-foo=no is equivalent to --without-foo
---
 configure | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/configure b/configure
index 1e17b46..c415568 100755
--- 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
-- 
2.1.4