Add an option -nodoc to configure, same (but shorter) than -with-doc no

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15962 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 4 insertions, 2 deletions

diff --git a/configure b/configure
index 56d118697..cb00667ac 100755
--- a/configure
+++ b/configure
@@ -74,8 +74,8 @@ usage () {
     printf "\tSpecifies to not try to build coqide mac integration\n"
     echo "-browser <command>"
     printf "\tUse <command> to open URL %%s\n"
-    echo "-with-doc (yes|no)"
-    printf "\tSpecifies whether or not to compile the documentation\n"
+    echo "-nodoc"
+    printf "\tSpecifies to not compile the documentation\n"
     echo "-with-geoproof (yes|no)"
     printf "\tSpecifies whether or not to use Geoproof binding\n"
     echo "-byte-only"
@@ -228,6 +228,8 @@ while : ; do
     -coqwebsite|--coqwebsite) wwwcoq_spec=yes
                       WWWCOQ=$2
                       shift;;
+    -nodoc|--nodoc) with_doc_spec=yes
+                    with_doc=no;;
     -with-doc|--with-doc) with_doc_spec=yes
 		      case "$2" in
 			  yes|all) with_doc=all;;