diff -r a8409fa3985c -r d7bb261e3a3b lib/Tools/document
--- 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"
 )