lib/Tools/document
changeset 12688 4ad13c2f7196
parent 11948 9c812b21b2e8
child 14344 0f0a2148a099
     1.1 --- a/lib/Tools/document	Wed Jan 09 17:36:18 2002 +0100
     1.2 +++ b/lib/Tools/document	Wed Jan 09 17:36:34 2002 +0100
     1.3 @@ -84,6 +84,7 @@
     1.4  {
     1.5    local FMT="$1"
     1.6    [ -n "$CLEAN" ] && rm -f *.aux *.out
     1.7 +  "$ISATOOL" latex -o sty && \
     1.8    "$ISATOOL" latex -o "$FMT" && \
     1.9    { [ ! -f root.bib ] || "$ISATOOL" latex -o bbl; } && \
    1.10    "$ISATOOL" latex -o "$FMT"