From 30076f81448721c49b86846de638cbc936c085fb Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Tue, 17 Feb 2015 21:38:13 +0100 Subject: Separate index for vernacular options. --- Makefile.doc | 2 ++ 1 file changed, 2 insertions(+) (limited to 'Makefile.doc') 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;\ -- cgit v1.2.3