--- 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="$?"