--- a/lib/Tools/document Sat Oct 20 20:14:56 2001 +0200
+++ b/lib/Tools/document Sat Oct 20 20:15:27 2001 +0200
@@ -18,7 +18,6 @@
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 " -v be verbose"
echo
echo " Prepare the theory session document in DIR (default 'document')"
echo " producing the specified output format."
@@ -39,9 +38,8 @@
CLEAN=""
OUTFORMAT=dvi
-VERBOSE=""
-while getopts "co:v" OPT
+while getopts "co:" OPT
do
case "$OPT" in
c)
@@ -50,9 +48,6 @@
o)
OUTFORMAT="$OPTARG"
;;
- v)
- VERBOSE=true
- ;;
\?)
usage
;;
@@ -122,8 +117,7 @@
fi
if [ "$RC" -eq 0 -a -f "root.$OUTFORMAT" ]; then
- cp -f "root.$OUTFORMAT" "../document.$OUTFORMAT" && \
- [ -n "$VERBOSE" ] && echo "$(cd ..; echo "Prepared $PWD/document.$OUTFORMAT")" >&2
+ cp -f "root.$OUTFORMAT" "../document.$OUTFORMAT"
fi
exit "$RC"