# HG changeset patch
# User wenzelm
# Date 1374957844 -7200
# Node ID 8e398d9bedf34282d5fff771d686544d25ad8b32
# Parent  2130b5c4b2873d43fed8814404d9e8a6cb24828d
more uniform cleanup;

diff -r 2130b5c4b287 -r 8e398d9bedf3 lib/Tools/document
--- a/lib/Tools/document	Sat Jul 27 22:38:06 2013 +0200
+++ b/lib/Tools/document	Sat Jul 27 22:44:04 2013 +0200
@@ -120,7 +120,7 @@
 (
   cd "$DIR" || fail "Bad directory '$DIR'"
 
-  [ -n "$CLEAN" ] && rm -f "../$NAME.$OUTFORMAT"
+  [ -n "$CLEAN" ] && rm -f "../$NAME.$OUTFORMAT" *.aux *.out *.ind *.idx *.ilg *.bbl *.blg *.log
 
   prep_tags
 
@@ -128,7 +128,6 @@
     ./build "$OUTFORMAT" "$NAME"
     RC="$?"
   else
-    [ -n "$CLEAN" ] && rm -f *.aux *.out *.ind *.idx *.ilg *.bbl *.blg *.log
     "$ISABELLE_TOOL" latex -o sty "$ROOT_NAME.tex" && \
     "$ISABELLE_TOOL" latex -o "$OUTFORMAT" "$ROOT_NAME.tex" && \
     { [ ! -f "$ROOT_NAME.bib" ] || "$ISABELLE_TOOL" latex -o bbl "$ROOT_NAME.tex"; } && \