diff options
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 33dd60dba..1f3509351 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;\ |