diff -r 3dc60e93064f -r eb072fd9a45a lib/Tools/document
--- 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"