lib/Tools/getenv
changeset 28650 a7ba12e0d3b7
parent 17226 0687c76021c0
child 29143 72c960b2b83e
     1.1 --- a/lib/Tools/getenv	Tue Oct 21 20:17:40 2008 +0200
     1.2 +++ b/lib/Tools/getenv	Tue Oct 21 20:18:07 2008 +0200
     1.3 @@ -13,7 +13,7 @@
     1.4  function usage()
     1.5  {
     1.6    echo
     1.7 -  echo "Usage: $PRG [OPTIONS] [VARNAMES ...]"
     1.8 +  echo "Usage: isabelle $PRG [OPTIONS] [VARNAMES ...]"
     1.9    echo
    1.10    echo "  Options are:"
    1.11    echo "    -a           display complete environment"