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