lib/Tools/install
changeset 28650 a7ba12e0d3b7
parent 28504 7ad7d7d6df47
child 28915 0642cbb60c98
     1.1 --- a/lib/Tools/install	Tue Oct 21 20:17:40 2008 +0200
     1.2 +++ b/lib/Tools/install	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]"
     1.8 +  echo "Usage: isabelle $PRG [OPTIONS]"
     1.9    echo
    1.10    echo "  Options are:"
    1.11    echo "    -d DISTDIR   refer to DISTDIR as Isabelle distribution"