# 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=$?