tuned usage;
authorwenzelm
Wed Oct 13 19:43:52 1999 +0200 (1999-10-13)
changeset 7857a49a3978fe3a
parent 7856 7d06972db6ca
child 7858 2cd88d1eec0c
tuned usage;
lib/Tools/document
lib/Tools/latex
     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  }
     2.1 --- a/lib/Tools/latex	Wed Oct 13 19:43:26 1999 +0200
     2.2 +++ b/lib/Tools/latex	Wed Oct 13 19:43:52 1999 +0200
     2.3 @@ -16,9 +16,8 @@
     2.4    echo "    -o FORMAT    specify output format: dvi (default), dvi.gz, ps, ps.gz,"
     2.5    echo "                 pdf, or bbl"
     2.6    echo
     2.7 -  echo
     2.8 -  echo "  Run LaTeX (and related tools) on FILE (default root.tex), producing the"
     2.9 -  echo "  speficied output format."
    2.10 +  echo "  Run LaTeX (and related tools) on FILE (default root.tex),"
    2.11 +  echo "  producing the specified output format."
    2.12    echo
    2.13    exit 1
    2.14  }