diff options
| author | Pierre-Marie Pédrot | 2015-02-18 17:27:39 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-02-18 17:27:39 +0100 |
| commit | 4bb062f4a66c4ae5a1742e7d99fdc335de0d57a9 (patch) | |
| tree | af8ead1cdc5af3842e683f602177ab4fa2dec9b5 /Makefile.doc | |
| parent | 1be9c4da4d814c29d4ba45b121fda924adc1130e (diff) | |
| parent | 29ba692f0fd25ce87392bbb7494cb62e3b97dc07 (diff) | |
Merge branch 'v8.5'
Diffstat (limited to 'Makefile.doc')
| -rw-r--r-- | Makefile.doc | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/Makefile.doc b/Makefile.doc index 33dd60dbad..1f35093510 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -99,6 +99,8 @@ doc/refman/Reference-Manual.dvi: $(REFMANFILES) doc/refman/Reference-Manual.tex $(SHOWMAKEINDEXERROR) Reference-Manual.ilg;\ $(MAKEINDEX) -q Reference-Manual.comidx -o Reference-Manual.comind;\ $(SHOWMAKEINDEXERROR) Reference-Manual.ilg;\ + $(MAKEINDEX) -q Reference-Manual.optidx -o Reference-Manual.optind;\ + $(SHOWMAKEINDEXERROR) Reference-Manual.ilg;\ $(MAKEINDEX) -q Reference-Manual.erridx -o Reference-Manual.errind;\ $(SHOWMAKEINDEXERROR) Reference-Manual.ilg;\ $(LATEX) -interaction=batchmode Reference-Manual > /dev/null;\ |