diff -r 75466ad27dd7 -r 25fb7241f32e lib/Tools/latex
--- a/lib/Tools/latex	Thu May 15 18:12:43 2008 +0200
+++ b/lib/Tools/latex	Thu May 15 20:02:37 2008 +0200
@@ -15,7 +15,7 @@
   echo
   echo "  Options are:"
   echo "    -o FORMAT    specify output format: dvi (default), dvi.gz, ps, ps.gz,"
-  echo "                 pdf, bbl, png, sty, syms"
+  echo "                 pdf, bbl, idx, sty, syms"
   echo
   echo "  Run LaTeX (and related tools) on FILE (default root.tex),"
   echo "  producing the specified output format."
@@ -77,7 +77,6 @@
 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 ()
 {
   for STYLEFILE in "$ISABELLE_HOME/lib/texinputs"/*.sty
@@ -137,11 +136,6 @@
     run_makeindex
     RC="$?"
     ;;
-  png)
-    check_root && \
-    run_thumbpdf
-    RC="$?"
-    ;;
   sty)
     copy_styles
     RC="$?"