diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-11-12 13:55:37 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-11-12 13:55:37 +0000 |
commit | c02eaa85a708bc9f45920e894aadfb73bdc183ae (patch) | |
tree | 555d642296880e46a9b056947ed85024cdd54380 | |
parent | 863b9fa00230b754458578857732b1e3a9e225f6 (diff) |
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
-rwxr-xr-x | configure | 6 |
1 files changed, 4 insertions, 2 deletions
@@ -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;; |