1 files changed, 39 insertions, 26 deletions
diff --git a/Makefile.build b/Makefile.build
index fe2bba29e..2dd8ec01b 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -584,12 +584,47 @@ install-latex:
 # Documentation of the source code (using ocamldoc)
 ###########################################################################
 
-.PHONY: source-doc
+.PHONY: source-doc mli-doc ml-doc
 
-source-doc:
-	if !(test -d $(SOURCEDOCDIR)); then mkdir $(SOURCEDOCDIR); fi
+source-doc: mli-doc $(OCAMLDOCDIR)/coq.pdf
+
+$(OCAMLDOCDIR)/coq.tex:: $(DOCMLIS:.mli=.cmi)
+	$(OCAMLDOC) -latex -rectypes -I /usr/lib/ocaml/camlp5 $(MLINCLUDES)\
+	$(DOCMLIS) -t "Coq mlis documentation" \
+	-intro $(OCAMLDOCDIR)/docintro -o $@
+
+mli-doc:: $(DOCMLIS:.mli=.cmi)
+	$(OCAMLDOC) -html -rectypes -I /usr/lib/ocaml/camlp5 $(MLINCLUDES)\
+	$(DOCMLIS) -d $(OCAMLDOCDIR)/html -colorize-code \
+	-t "Coq mlis documentation" -intro $(OCAMLDOCDIR)/docintro \
+	-css-style style.css
+
+%.png: %.dot
+	$(DOT) -Tpng $< -o $@
+
+%.types.dot: %.mli
+	$(OCAMLDOC) -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -dot-types -o $@ $< 
+
+OCAMLDOC_MLLIBD = $(OCAMLDOC) -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ \
+  `cat $| | tr ' ' '\n' | sed -n -e "/\.cmo/s/\.cmo/\.ml/p"`
+
+%.dot: | %.mllib.d
+	$(OCAMLDOC_MLLIBD)
+
+ml-doc:
 	$(OCAMLDOC) -html -rectypes $(LOCALINCLUDES) -d $(SOURCEDOCDIR) $(MLSTATICFILES)
 
+parsing/parsing.dot : | parsing/parsing.mllib.d parsing/highparsing.mllib.d
+	$(OCAMLDOC_MLLIBD)
+
+tactics/tactics.dot: | tactics/tactics.mllib.d tactics/hightactics.mllib.d
+	$(OCAMLDOC_MLLIBD)
+
+%.dot: %.mli
+	$(OCAMLDOC) -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ $< 
+
+$(OCAMLDOCDIR)/%.pdf: $(OCAMLDOCDIR)/%.tex
+	(cd $(OCAMLDOCDIR) ; pdflatex $*.tex && pdflatex $*.tex)
 
 ###########################################################################
 ### Special rules
@@ -657,7 +692,7 @@ ifeq ($(CHECKEDOUT),git)
 	if test -x "`which git`"; then \
 	  LANG=C; export LANG; \
 	  GIT_BRANCH=$$(git branch -a | sed -ne '/^\* /s/^\* \(.*\)/\1/p'); \
-	  GIT_HOST=$$(hostname -f); \
+	  GIT_HOST=$$(hostname); \
 	  GIT_PATH=$$(pwd); \
 	  (echo "$${GIT_HOST}:$${GIT_PATH},$${GIT_BRANCH}") > revision.new; \
 	  (echo "$$(git log -1 --pretty='format:%H')") >> revision.new; \
@@ -822,28 +857,6 @@ devel: $(DEBUGPRINTERS)
 ###########################################################################
 
 
-%.types.dot: %.mli
-	$(OCAMLDOC) -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -dot-types -o $@ $< 
-
-%.dep.ps: %.dot
-	$(DOT) $(DOTOPTS) -o $@ $<
-
-OCAMLDOC_MLLIBD = $(OCAMLDOC) -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ \
-  `cat $| | tr ' ' '\n' | sed -n -e "/\.cmo/s/\.cmo/\.ml/p"`
-
-%.dot: | %.mllib.d
-	$(OCAMLDOC_MLLIBD)
-
-parsing/parsing.dot : | parsing/parsing.mllib.d parsing/highparsing.mllib.d
-	$(OCAMLDOC_MLLIBD)
-
-tactics/tactics.dot: | tactics/tactics.mllib.d tactics/hightactics.mllib.d
-	$(OCAMLDOC_MLLIBD)
-
-%.dot: %.mli
-	$(OCAMLDOC) -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) -o $@ $< 
-
-
 # For emacs: 
 # Local Variables: 
 # mode: makefile