lib/Tools/document
changeset 7857 a49a3978fe3a
parent 7814 ef6d84f16592
child 7866 3ccaa11b6df9
     1.1 --- a/lib/Tools/document	Wed Oct 13 19:43:26 1999 +0200
     1.2 +++ b/lib/Tools/document	Wed Oct 13 19:43:52 1999 +0200
     1.3 @@ -15,9 +15,8 @@
     1.4    echo "  Options are:"
     1.5    echo "    -o FORMAT    specify output format: dvi (default), dvi.gz, ps, ps.gz, pdf"
     1.6    echo
     1.7 -  echo
     1.8 -  echo "  Prepare the theory session document in DIR (default .)"
     1.9 -  echo "  producing the speficied output format."
    1.10 +  echo "  Prepare the theory session document in DIR (default '.')"
    1.11 +  echo "  producing the specified output format."
    1.12    echo
    1.13    exit 1
    1.14  }