1.1 --- a/lib/Tools/latex	Thu May 15 18:12:43 2008 +0200
     1.2 +++ b/lib/Tools/latex	Thu May 15 20:02:37 2008 +0200
     1.3 @@ -15,7 +15,7 @@
     1.4    echo
     1.5    echo "  Options are:"
     1.6    echo "    -o FORMAT    specify output format: dvi (default), dvi.gz, ps, ps.gz,"
     1.7 -  echo "                 pdf, bbl, png, sty, syms"
     1.8 +  echo "                 pdf, bbl, idx, sty, syms"
     1.9    echo
    1.10    echo "  Run LaTeX (and related tools) on FILE (default root.tex),"
    1.11    echo "  producing the specified output format."
    1.12 @@ -77,7 +77,6 @@
    1.13  function run_bibtex () { $ISABELLE_BIBTEX </dev/null "$FILEBASE"; }
    1.14  function run_makeindex () { $ISABELLE_MAKEINDEX </dev/null "$FILEBASE"; }
    1.15  function run_dvips () { $ISABELLE_DVIPS -q -o "$FILEBASE.ps" "$FILEBASE.dvi"; }
    1.16 -function run_thumbpdf () { [ -n "$ISABELLE_THUMBPDF" ] && $ISABELLE_THUMBPDF "$FILEBASE"; }
    1.17  function copy_styles ()
    1.18  {
    1.19    for STYLEFILE in "$ISABELLE_HOME/lib/texinputs"/*.sty
    1.20 @@ -137,11 +136,6 @@
    1.21      run_makeindex
    1.22      RC="$?"
    1.23      ;;
    1.24 -  png)
    1.25 -    check_root && \
    1.26 -    run_thumbpdf
    1.27 -    RC="$?"
    1.28 -    ;;
    1.29    sty)
    1.30      copy_styles
    1.31      RC="$?"