# HG changeset patch
# User wenzelm
# Date 950095724 -3600
# Node ID dc3b8cdbb816688a24436c94d6428c9a49347998
# Parent  e4b3192dfefad55601be16f0d66f0ac4dc865740
option -c;

diff -r e4b3192dfefa -r dc3b8cdbb816 lib/Tools/document
--- a/lib/Tools/document	Wed Feb 09 11:45:10 2000 +0100
+++ b/lib/Tools/document	Wed Feb 09 12:28:44 2000 +0100
@@ -13,7 +13,7 @@
   echo "Usage: $PRG [OPTIONS] [DIR]"
   echo
   echo "  Options are:"
-  echo "    -c           clean -- remove DIR after succesful run"
+  echo "    -c           remove DIR after succesful run (!)"
   echo "    -o FORMAT    specify output format: dvi (default), dvi.gz, ps,"
   echo "                 ps.gz, pdf"
   echo
@@ -115,7 +115,7 @@
   [ "$RC" -eq 0 -a -f "root.$OUTFORMAT" ] && \
     cp -f "root.$OUTFORMAT" "../document.$OUTFORMAT"
 
-  exit $RC
+  exit "$RC"
 )
 RC=$?