From a57b3d43033103a1efda78ab2e5f273c217a1834 Mon Sep 17 00:00:00 2001 From: David Bremner Date: Thu, 30 Jul 2015 08:08:31 +0200 Subject: [PATCH] configure: support --with-docs=no 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 1e17b464..c415568c 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