lib/Tools/document
changeset 28650 a7ba12e0d3b7
parent 28500 4b79e5d3d0aa
child 29143 72c960b2b83e
     1.1 --- a/lib/Tools/document	Tue Oct 21 20:17:40 2008 +0200
     1.2 +++ b/lib/Tools/document	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] [DIR]"
     1.8 +  echo "Usage: isabelle $PRG [OPTIONS] [DIR]"
     1.9    echo
    1.10    echo "  Options are:"
    1.11    echo "    -c           cleanup -- be aggressive in removing old stuff"