1.1 --- a/lib/Tools/document	Thu May 15 18:12:43 2008 +0200
     1.2 +++ b/lib/Tools/document	Thu May 15 20:02:37 2008 +0200
     1.3 @@ -139,10 +139,6 @@
     1.4    elif [ "$OUTFORMAT" = pdf ]; then
     1.5      pre_latex pdf && \
     1.6      "$ISATOOL" latex -o pdf && \
     1.7 -    { if [ -n "$ISABELLE_THUMBPDF" ]; then
     1.8 -        "$ISATOOL" latex -o png && \
     1.9 -        "$ISATOOL" latex -o pdf
    1.10 -      fi; }
    1.11      RC="$?"
    1.12    else
    1.13      pre_latex dvi && \