diff options
| author |  mrmr1993 <mr_1993@hotmail.co.uk> | 2018-02-27 12:03:34 +0000 |
|---|---|---|
| committer | mrmr1993 <mr_1993@hotmail.co.uk> | 2018-02-27 12:03:34 +0000 |
| commit | 30218fbe65732f3352d52599dbd1a1d17cc23644 (patch) | |
| tree | 4744b6c3c4a936b3104ee458a31c50cdea7b9dc8 /Makefile.doc | |
| parent | 9238db3009b3007d6b6a3767a9232088b8c88b9b (diff) | |
Use relative path for show_latex_messages
Diffstat (limited to 'Makefile.doc')
| -rw-r--r-- | Makefile.doc | 2 |
1 files changed, 1 insertions, 1 deletions
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 |