--- a/lib/Tools/document Thu Sep 27 12:24:19 2001 +0200
+++ b/lib/Tools/document Thu Sep 27 12:24:40 2001 +0200
@@ -18,6 +18,7 @@
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."
@@ -38,8 +39,9 @@
CLEAN=""
OUTFORMAT=dvi
+VERBOSE=""
-while getopts "co:" OPT
+while getopts "co:v" OPT
do
case "$OPT" in
c)
@@ -48,6 +50,9 @@
o)
OUTFORMAT="$OPTARG"
;;
+ v)
+ VERBOSE=true
+ ;;
\?)
usage
;;
@@ -116,8 +121,10 @@
RC="$?"
fi
- [ "$RC" -eq 0 -a -f "root.$OUTFORMAT" ] && \
- cp -f "root.$OUTFORMAT" "../document.$OUTFORMAT"
+ 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
+ fi
exit "$RC"
)