diff -r 7d06972db6ca -r a49a3978fe3a lib/Tools/document
--- a/lib/Tools/document	Wed Oct 13 19:43:26 1999 +0200
+++ b/lib/Tools/document	Wed Oct 13 19:43:52 1999 +0200
@@ -15,9 +15,8 @@
   echo "  Options are:"
   echo "    -o FORMAT    specify output format: dvi (default), dvi.gz, ps, ps.gz, pdf"
   echo
-  echo
-  echo "  Prepare the theory session document in DIR (default .)"
-  echo "  producing the speficied output format."
+  echo "  Prepare the theory session document in DIR (default '.')"
+  echo "  producing the specified output format."
   echo
   exit 1
 }