support thumbpdf (via 'png' output format);
authorwenzelm
Thu Oct 14 15:03:34 1999 +0200 (1999-10-14)
changeset 7865d9be8bc5624e
parent 7864 5cd5a27f5c93
child 7866 3ccaa11b6df9
support thumbpdf (via 'png' output format);
lib/Tools/latex
     1.1 --- a/lib/Tools/latex	Thu Oct 14 15:02:04 1999 +0200
     1.2 +++ b/lib/Tools/latex	Thu Oct 14 15:03:34 1999 +0200
     1.3 @@ -14,7 +14,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, or bbl"
     1.8 +  echo "                 pdf, bbl, png"
     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 @@ -78,6 +78,7 @@
    1.13  function run_pdflatex () { $ISABELLE_PDFLATEX "\\nonstopmode\\input{$FILEBASE.tex}"; }
    1.14  function run_bibtex () { $ISABELLE_BIBTEX </dev/null "$FILEBASE"; }
    1.15  function run_dvips () { $ISABELLE_DVIPS -o "$FILEBASE.ps" "$FILEBASE.dvi"; }
    1.16 +function run_thumbpdf () { [ -n "$ISABELLE_THUMBPDF" ] && $ISABELLE_THUMBPDF "$FILEBASE"; }
    1.17  
    1.18  
    1.19  # process file
    1.20 @@ -111,6 +112,10 @@
    1.21      run_bibtex
    1.22      RC=$?
    1.23      ;;
    1.24 +  png)
    1.25 +    run_thumbpdf
    1.26 +    RC=$?
    1.27 +    ;;
    1.28    *)
    1.29      fail "Bad output format '$OUTFORMAT'"
    1.30      ;;