--- 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 </dev/null "$FILEBASE"; }
+function run_makeindex () { $ISABELLE_MAKEINDEX </dev/null "$FILEBASE"; }
function run_dvips () { $ISABELLE_DVIPS -q -o "$FILEBASE.ps" "$FILEBASE.dvi"; }
function run_thumbpdf () { [ -n "$ISABELLE_THUMBPDF" ] && $ISABELLE_THUMBPDF "$FILEBASE"; }
function copy_styles () { cp -f "$ISABELLE_HOME/lib/texinputs"/*.sty "$DIR"; }
@@ -115,6 +116,11 @@
run_bibtex
RC="$?"
;;
+ idx)
+ check_root && \
+ run_makeindex
+ RC="$?"
+ ;;
png)
check_root && \
run_thumbpdf