From 30218fbe65732f3352d52599dbd1a1d17cc23644 Mon Sep 17 00:00:00 2001
From: mrmr1993 <mr_1993@hotmail.co.uk>
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(-)

(limited to 'Makefile.doc')

diff --git a/Makefile.doc b/Makefile.doc
index db4cb6a58..3385e4951 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