--- 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
}
--- 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
}