changeset 28506 | 3ab515ee4e6f |
parent 28504 | 7ad7d7d6df47 |
child 28934 | 801098c96f59 |
--- a/bin/isabelle Sat Oct 04 17:40:58 2008 +0200 +++ b/bin/isabelle Sat Oct 04 17:50:57 2008 +0200 @@ -24,10 +24,9 @@ function usage() { echo - echo "Usage: $PRG TOOL [ARGS ...]" + echo "Usage: $PRG NAME [ARGS ...]" echo - echo " Start Isabelle utility program TOOL with ARGS. Pass \"-?\" to TOOL" - echo " for more specific help." + echo " Start Isabelle tool NAME with ARGS; pass \"-?\" for tool specific help." echo echo " Available tools are:" (