From 9238db3009b3007d6b6a3767a9232088b8c88b9b Mon Sep 17 00:00:00 2001
From: mrmr1993
Date: Tue, 27 Feb 2018 11:58:20 +0000
Subject: Use MYCAMLP5LIB instead of undefined MYCAMLP4LIB

This completes the work of
b60906cc3ee3f994babf9cceff2971bd03485f2f
---
 Makefile.doc | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/Makefile.doc b/Makefile.doc
index 8cb9c9f0fa..db4cb6a58b 100644
--- a/Makefile.doc
+++ b/Makefile.doc
@@ -400,7 +400,7 @@ source-doc: mli-doc $(OCAMLDOCDIR)/coq.pdf
 
 $(OCAMLDOCDIR)/coq.tex: $(DOCMLIS:.mli=.cmi)
 	$(SHOW)'OCAMLDOC -latex -o $@'
-	$(HIDE)$(OCAMLFIND) ocamldoc -latex -rectypes -I $(MYCAMLP4LIB) $(MLINCLUDES)\
+	$(HIDE)$(OCAMLFIND) ocamldoc -latex -rectypes -I $(MYCAMLP5LIB) $(MLINCLUDES)\
 	$(DOCMLIS) -noheader -t "Coq mlis documentation" \
 	-intro $(OCAMLDOCDIR)/docintro -o $@.tmp
 	$(SHOW)'OCAMLDOC utf8 fix'
@@ -410,13 +410,13 @@ $(OCAMLDOCDIR)/coq.tex: $(DOCMLIS:.mli=.cmi)
 
 mli-doc: $(DOCMLIS:.mli=.cmi)
 	$(SHOW)'OCAMLDOC -html'
-	$(HIDE)$(OCAMLFIND) ocamldoc -charset utf-8 -html -rectypes -I +threads -I $(MYCAMLP4LIB) $(MLINCLUDES) \
+	$(HIDE)$(OCAMLFIND) ocamldoc -charset utf-8 -html -rectypes -I +threads -I $(MYCAMLP5LIB) $(MLINCLUDES) \
 	$(DOCMLIS) -d $(OCAMLDOCDIR)/html -colorize-code \
 	-t "Coq mlis documentation" -intro $(OCAMLDOCDIR)/docintro \
 	-css-style style.css
 
 ml-dot: $(MLFILES)
-	$(OCAMLFIND) ocamldoc -dot -dot-reduce -rectypes -I +threads -I $(CAMLLIB) -I $(MYCAMLP4LIB) $(MLINCLUDES) \
+	$(OCAMLFIND) ocamldoc -dot -dot-reduce -rectypes -I +threads -I $(CAMLLIB) -I $(MYCAMLP5LIB) $(MLINCLUDES) \
 	$(filter $(addsuffix /%.ml,$(CORESRCDIRS)),$(MLFILES)) -o $(OCAMLDOCDIR)/coq.dot
 
 %_dep.png: %.dot
-- 
cgit v1.2.3


From 30218fbe65732f3352d52599dbd1a1d17cc23644 Mon Sep 17 00:00:00 2001
From: mrmr1993
Date: Tue, 27 Feb 2018 12:03:34 +0000
Subject: Use relative path for show_latex_messages

---
 Makefile.doc | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Makefile.doc b/Makefile.doc
index db4cb6a58b..3385e4951d 100644
--- a/Makefile.doc
+++ b/Makefile.doc
@@ -449,7 +449,7 @@ tactics/tactics.dot: | tactics/tactics.mllib.d ltac/ltac.mllib.d
 $(OCAMLDOCDIR)/%.pdf: $(OCAMLDOCDIR)/%.tex
 	$(SHOW)'PDFLATEX $*.tex'
 	$(HIDE)(cd $(OCAMLDOCDIR) ; pdflatex -interaction=batchmode $*.tex && pdflatex -interaction=batchmode $*.tex)
-	$(HIDE)(cd doc/tools/; show_latex_messages -no-overfull ../../$(OCAMLDOCDIR)/$*.log)
+	$(HIDE)(cd doc/tools/; ./show_latex_messages -no-overfull ../../$(OCAMLDOCDIR)/$*.log)
 
 ###########################################################################
 # local web server
-- 
cgit v1.2.3