Ajout d'une option pour contrôler l'installation automatique de la documentation + ajout d'un test pour hevea et latex

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

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
 
diff --git a/configure b/configure
index 80e311e55..adbea2493 100755
--- a/configure
+++ b/configure
@@ -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"