# HG changeset patch
# User wenzelm
# Date 939836632 -7200
# Node ID a49a3978fe3adb8a3e8b04a9369090cb2ed4a0cd
# Parent  7d06972db6caaef9569dccf0128d4d4a5dc2b890
tuned usage;

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
 }
diff -r 7d06972db6ca -r a49a3978fe3a lib/Tools/latex
--- a/lib/Tools/latex	Wed Oct 13 19:43:26 1999 +0200
+++ b/lib/Tools/latex	Wed Oct 13 19:43:52 1999 +0200
@@ -16,9 +16,8 @@
   echo "    -o FORMAT    specify output format: dvi (default), dvi.gz, ps, ps.gz,"
   echo "                 pdf, or bbl"
   echo
-  echo
-  echo "  Run LaTeX (and related tools) on FILE (default root.tex), producing the"
-  echo "  speficied output format."
+  echo "  Run LaTeX (and related tools) on FILE (default root.tex),"
+  echo "  producing the specified output format."
   echo
   exit 1
 }