# HG changeset patch # User kleing # Date 1073532772 -3600 # Node ID 0f0a2148a099d7e9421f97911c2bcdf7c479280b # Parent 6bc647f472b9c2bce588520b85bec0fc58ad188d run makeindex if necessary diff -r 6bc647f472b9 -r 0f0a2148a099 etc/settings --- a/etc/settings Wed Jan 07 07:52:12 2004 +0100 +++ b/etc/settings Thu Jan 08 04:32:52 2004 +0100 @@ -85,6 +85,9 @@ # bibtex command for isatool latex/document ISABELLE_BIBTEX="bibtex" +# makeindex command for isatool latex/document +ISABELLE_MAKEINDEX="makeindex" + # dvips command for isatool latex/document ISABELLE_DVIPS="dvips -D 600" diff -r 6bc647f472b9 -r 0f0a2148a099 lib/Tools/document --- a/lib/Tools/document Wed Jan 07 07:52:12 2004 +0100 +++ b/lib/Tools/document Thu Jan 08 04:32:52 2004 +0100 @@ -83,11 +83,12 @@ function pre_latex () { local FMT="$1" - [ -n "$CLEAN" ] && rm -f *.aux *.out + [ -n "$CLEAN" ] && rm -f *.aux *.out *.ind "$ISATOOL" latex -o sty && \ "$ISATOOL" latex -o "$FMT" && \ { [ ! -f root.bib ] || "$ISATOOL" latex -o bbl; } && \ - "$ISATOOL" latex -o "$FMT" + { [ ! -f root.idx ] || "$ISATOOL" latex -o idx; } && \ + "$ISATOOL" latex -o "$FMT" } ( diff -r 6bc647f472b9 -r 0f0a2148a099 lib/Tools/latex --- a/lib/Tools/latex Wed Jan 07 07:52:12 2004 +0100 +++ b/lib/Tools/latex Thu Jan 08 04:32:52 2004 +0100 @@ -76,6 +76,7 @@ function run_latex () { $ISABELLE_LATEX "\\nonstopmode\\input{$FILEBASE.tex}"; } function run_pdflatex () { $ISABELLE_PDFLATEX "\\nonstopmode\\input{$FILEBASE.tex}"; } function run_bibtex () { $ISABELLE_BIBTEX