changeset 7857 | a49a3978fe3a |
parent 7814 | ef6d84f16592 |
child 7866 | 3ccaa11b6df9 |
--- 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 }