equal
deleted
inserted
replaced
18 function usage() |
18 function usage() |
19 { |
19 { |
20 echo |
20 echo |
21 echo "Usage: $PRG TOOL [ARGS ...]" |
21 echo "Usage: $PRG TOOL [ARGS ...]" |
22 echo |
22 echo |
23 echo " Start Isabelle utility program TOOL with ARGS." |
23 echo " Start Isabelle utility program TOOL with ARGS. Pass \"-?\" to TOOL" |
|
24 echo " for specific help." |
24 echo |
25 echo |
25 echo " Availabe tools are:" |
26 echo " Availabe tools are:" |
|
27 echo |
26 ( |
28 ( |
27 cd "$ISABELLE_HOME/lib/Tools" |
29 cd "$ISABELLE_HOME/lib/Tools" |
28 for T in * |
30 for T in * |
29 do |
31 do |
30 if [ -f "$T" -a -x "$T" ]; then |
32 if [ -f "$T" -a -x "$T" ]; then |