# HG changeset patch
# User wenzelm
# Date 954613016 -7200
# Node ID 38ce936acb994bbffdb8e32ca1802c93f545d259
# Parent  a88e91792f0ac6b4b6ca69c1fea745e6f41925d8
tuned -c option;

diff -r a88e91792f0a -r 38ce936acb99 lib/Tools/document
--- a/lib/Tools/document	Sat Apr 01 20:15:55 2000 +0200
+++ b/lib/Tools/document	Sat Apr 01 20:16:56 2000 +0200
@@ -13,7 +13,7 @@
   echo "Usage: $PRG [OPTIONS] [DIR]"
   echo
   echo "  Options are:"
-  echo "    -c           remove DIR after succesful run (!)"
+  echo "    -c           cleanup -- be aggressive in removing old stuff"
   echo "    -o FORMAT    specify output format: dvi (default), dvi.gz, ps,"
   echo "                 ps.gz, pdf"
   echo
@@ -81,7 +81,7 @@
 function pre_latex ()
 {
   local FMT="$1"
-  rm -f *.aux *.out
+  [ -n "$CLEAN" ] && rm -f *.aux *.out
   if [ -f root.bib ]
   then
     $ISATOOL latex -o "$FMT" && \
@@ -95,6 +95,8 @@
 (
   cd "$DIR" || fail "Bad directory '$DIR'"
 
+  [ -n "$CLEAN" ] && rm -f "../document.$OUTFORMAT"
+
   if [ -f IsaMakefile ]; then
     $ISATOOL make "$OUTFORMAT"
     RC=$?