bin/isatool
changeset 3276 f8bf5e5c1641
parent 3007 e5efa177ee0c
child 7971 023778c8a029
equal deleted inserted replaced
3275:3f53f2c876f4 3276:f8bf5e5c1641
    25   echo "Usage: $PRG TOOL [ARGS ...]"
    25   echo "Usage: $PRG TOOL [ARGS ...]"
    26   echo
    26   echo
    27   echo "  Start Isabelle utility program TOOL with ARGS. Pass \"-?\" to TOOL"
    27   echo "  Start Isabelle utility program TOOL with ARGS. Pass \"-?\" to TOOL"
    28   echo "  for more specific help."
    28   echo "  for more specific help."
    29   echo
    29   echo
    30   echo "  Availabe tools are:"
    30   echo "  Available tools are:"
    31   (
    31   (
    32     for DIR in $TOOLDIRS
    32     for DIR in $TOOLDIRS
    33     do
    33     do
    34       cd $DIR
    34       cd $DIR
    35       echo
    35       echo