| changeset 28650 | a7ba12e0d3b7 |
| parent 28638 | 809dda85079d |
| child 29143 | 72c960b2b83e |
| 28649:58ab885469f5 | 28650:a7ba12e0d3b7 |
|---|---|
11 PRG="$(basename "$0")" |
11 PRG="$(basename "$0")" |
12 |
12 |
13 function usage() |
13 function usage() |
14 { |
14 { |
15 echo |
15 echo |
16 echo "Usage: $PRG [CMDLINE ...]" |
16 echo "Usage: isabelle $PRG [CMDLINE ...]" |
17 echo |
17 echo |
18 echo |
18 echo |
19 echo " Run CMDLINE within the Isabelle environment (via the system's env command)." |
19 echo " Run CMDLINE within the Isabelle environment (via the system's env command)." |
20 echo |
20 echo |
21 exit 1 |
21 exit 1 |