# HG changeset patch
# User wenzelm
# Date 954613132 -7200
# Node ID 1062572b5b3700082eceaccc64805df97b10db85
# Parent  16906e600c9afd09bae796f0d9b8c001e19c11a2
isatool document: tuned -c option;

diff -r 16906e600c9a -r 1062572b5b37 doc-src/System/present.tex
--- a/doc-src/System/present.tex	Sat Apr 01 20:17:51 2000 +0200
+++ b/doc-src/System/present.tex	Sat Apr 01 20:18:52 2000 +0200
@@ -254,7 +254,7 @@
 Usage: document [OPTIONS] [DIR]
 
   Options are:
-    -c           remove DIR after succesful run (!)
+    -c           cleanup -- be aggressive in removing old stuff
     -o FORMAT    specify output format: dvi (default), dvi.gz, ps,
                  ps.gz, pdf