lib/Tools/document
changeset 7866 3ccaa11b6df9
parent 7857 a49a3978fe3a
child 8171 f89329974d2d
     1.1 --- a/lib/Tools/document	Thu Oct 14 15:03:34 1999 +0200
     1.2 +++ b/lib/Tools/document	Thu Oct 14 15:04:36 1999 +0200
     1.3 @@ -13,7 +13,8 @@
     1.4    echo "Usage: $PRG [OPTIONS] [DIR]"
     1.5    echo
     1.6    echo "  Options are:"
     1.7 -  echo "    -o FORMAT    specify output format: dvi (default), dvi.gz, ps, ps.gz, pdf"
     1.8 +  echo "    -o FORMAT    specify output format: dvi (default), dvi.gz, ps,"
     1.9 +  echo "                 ps.gz, pdf"
    1.10    echo
    1.11    echo "  Prepare the theory session document in DIR (default '.')"
    1.12    echo "  producing the specified output format."
    1.13 @@ -92,7 +93,11 @@
    1.14    RC=$?   #FIXME !??
    1.15  elif [ "$OUTFORMAT" = pdf ]; then
    1.16    pre_latex pdf && \
    1.17 -  $ISATOOL latex -o pdf
    1.18 +  $ISATOOL latex -o pdf && \
    1.19 +  { if [ -n "$ISABELLE_THUMBPDF" ]; then
    1.20 +      $ISATOOL latex -o png && \
    1.21 +      $ISATOOL latex -o pdf
    1.22 +    fi; }
    1.23    RC=$?
    1.24  else
    1.25    pre_latex dvi && \