lib/Tools/latex
changeset 14344 0f0a2148a099
parent 12846 0fce95478e19
child 14921 4ad751fa50c1
     1.1 --- a/lib/Tools/latex	Wed Jan 07 07:52:12 2004 +0100
     1.2 +++ b/lib/Tools/latex	Thu Jan 08 04:32:52 2004 +0100
     1.3 @@ -76,6 +76,7 @@
     1.4  function run_latex () { $ISABELLE_LATEX "\\nonstopmode\\input{$FILEBASE.tex}"; }
     1.5  function run_pdflatex () { $ISABELLE_PDFLATEX "\\nonstopmode\\input{$FILEBASE.tex}"; }
     1.6  function run_bibtex () { $ISABELLE_BIBTEX </dev/null "$FILEBASE"; }
     1.7 +function run_makeindex () { $ISABELLE_MAKEINDEX </dev/null "$FILEBASE"; }
     1.8  function run_dvips () { $ISABELLE_DVIPS -q -o "$FILEBASE.ps" "$FILEBASE.dvi"; }
     1.9  function run_thumbpdf () { [ -n "$ISABELLE_THUMBPDF" ] && $ISABELLE_THUMBPDF "$FILEBASE"; }
    1.10  function copy_styles () { cp -f "$ISABELLE_HOME/lib/texinputs"/*.sty "$DIR"; }
    1.11 @@ -115,6 +116,11 @@
    1.12      run_bibtex
    1.13      RC="$?"
    1.14      ;;
    1.15 +  idx)
    1.16 +    check_root && \
    1.17 +    run_makeindex
    1.18 +    RC="$?"
    1.19 +    ;;
    1.20    png)
    1.21      check_root && \
    1.22      run_thumbpdf