lib/Tools/latex
changeset 28650 a7ba12e0d3b7
parent 26979 c58778bdf146
child 29143 72c960b2b83e
     1.1 --- a/lib/Tools/latex	Tue Oct 21 20:17:40 2008 +0200
     1.2 +++ b/lib/Tools/latex	Tue Oct 21 20:18:07 2008 +0200
     1.3 @@ -11,7 +11,7 @@
     1.4  function usage()
     1.5  {
     1.6    echo
     1.7 -  echo "Usage: $PRG [OPTIONS] [FILE]"
     1.8 +  echo "Usage: isabelle $PRG [OPTIONS] [FILE]"
     1.9    echo
    1.10    echo "  Options are:"
    1.11    echo "    -o FORMAT    specify output format: dvi (default), dvi.gz, ps, ps.gz,"