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 </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