diff options
-rw-r--r-- | Makefile.build | 5 | ||||
-rw-r--r-- | config/Makefile.template | 3 | ||||
-rwxr-xr-x | configure | 34 |
3 files changed, 42 insertions, 0 deletions
diff --git a/Makefile.build b/Makefile.build index a0035c78e..a90eb0eb9 100644 --- a/Makefile.build +++ b/Makefile.build @@ -36,7 +36,12 @@ NOARG: world # build and install the three subsystems: coq, coqide, pcoq world: revision coq coqide pcoq +ifeq ($(WITHDOC),all) install: install-coq install-coqide install-pcoq install-doc +else +install: install-coq install-coqide install-pcoq +endif + #install-manpages: install-coq-manpages install-pcoq-manpages ########################################################################### diff --git a/config/Makefile.template b/config/Makefile.template index e5061ebe8..fc8af173f 100644 --- a/config/Makefile.template +++ b/config/Makefile.template @@ -141,6 +141,9 @@ DOT=dot DOTOPTS=-Tps ODOCDOTOPTS=-dot -dot-reduce +# Option to control compilation and installation of the documentation +WITHDOC=WITHDOCOPT + # make or sed are bogus and believe lines not terminating by a return # are inexistent @@ -57,6 +57,8 @@ usage () { printf "\tSpecifies whether or not to compile full FSets/Reals library\n" echo "-coqide (opt|byte|no)" printf "\tSpecifies whether or not to compile Coqide\n" + echo "-with-doc (yes|no)" + printf "\tSpecifies whether or not to compile the documentation\n" echo "-with-geoproof (yes|no)" printf "\tSpecifies whether or not to use Geoproof binding\n" echo "-with-cc <file>" @@ -114,6 +116,8 @@ reals=all arch_spec=no coqide_spec=no with_geoproof=false +with_doc=all +with_doc_spec=no COQSRC=`pwd` @@ -183,6 +187,12 @@ while : ; do *) COQIDE=no esac shift;; + -with-doc|--with-doc) with_doc_spec=yes + case "$2" in + yes|all) with_doc=all;; + *) with_doc=no + esac + shift;; -with-geoproof|--with-geoproof) case $2 in yes) with_geoproof=true;; @@ -594,6 +604,24 @@ esac # "") MKTEXLSR=true;; #esac +# " +### Test if documentation can be compiled (latex, hevea) + +if test "$with_doc" = "all" +then + if test "`which latex`" = "" + then + echo "latex was not found; documentation will not be available" + with_doc=no + else + if test "`which hevea`" = "" + then + with_doc=no + echo "hevea was not found: documentation will not be available" + fi + fi +fi + ########################################### # bindir, libdir, mandir, docdir, etc. @@ -747,6 +775,11 @@ echo " Reals theory : All" else echo " Reals theory : Basic" fi +if test "$with_doc" = "all"; then +echo " Documentation : All" +else +echo " Documentation : None" +fi echo " CoqIde : $COQIDE" echo "" @@ -895,6 +928,7 @@ sed -e "s|LOCALINSTALLATION|$local|" \ -e "s|REALSOPT|$reals|" \ -e "s|COQIDEOPT|$COQIDE|" \ -e "s|CHECKEDOUTSOURCETREE|$checkedout|" \ + -e "s|WITHDOCOPT|$with_doc|" \ "$COQSRC/config/Makefile.template" > "$COQSRC/config/Makefile" chmod a-w "$COQSRC/config/Makefile" |