| changeset 28650 | a7ba12e0d3b7 |
| parent 28500 | 4b79e5d3d0aa |
| child 29143 | 72c960b2b83e |
| 28649:58ab885469f5 | 28650:a7ba12e0d3b7 |
|---|---|
8 PRG="$(basename "$0")" |
8 PRG="$(basename "$0")" |
9 |
9 |
10 function usage() |
10 function usage() |
11 { |
11 { |
12 echo |
12 echo |
13 echo "Usage: $PRG NAME" |
13 echo "Usage: isabelle $PRG NAME" |
14 echo |
14 echo |
15 echo " Prepare a session directory for PG-Eclipse." |
15 echo " Prepare a session directory for PG-Eclipse." |
16 exit 1 |
16 exit 1 |
17 } |
17 } |
18 |
18 |