diff -r a44fd835df98 -r 4ad13c2f7196 lib/Tools/document --- a/lib/Tools/document Wed Jan 09 17:36:18 2002 +0100 +++ b/lib/Tools/document Wed Jan 09 17:36:34 2002 +0100 @@ -84,6 +84,7 @@ { local FMT="$1" [ -n "$CLEAN" ] && rm -f *.aux *.out + "$ISATOOL" latex -o sty && \ "$ISATOOL" latex -o "$FMT" && \ { [ ! -f root.bib ] || "$ISATOOL" latex -o bbl; } && \ "$ISATOOL" latex -o "$FMT"