| changeset 10511 | efb3428c9879 |
| parent 9788 | df671fa2562a |
| child 10555 | 2323ec838401 |
| 10510:d243553849ec | 10511:efb3428c9879 |
|---|---|
5 # License: GPL (GNU GENERAL PUBLIC LICENSE) |
5 # License: GPL (GNU GENERAL PUBLIC LICENSE) |
6 # |
6 # |
7 # DESCRIPTION: create an instance of the Isabelle logo |
7 # DESCRIPTION: create an instance of the Isabelle logo |
8 |
8 |
9 |
9 |
10 PRG=$(basename "$0") |
10 PRG="$(basename "$0")" |
11 |
11 |
12 function usage() |
12 function usage() |
13 { |
13 { |
14 echo |
14 echo |
15 echo "Usage: $PRG [OPTIONS] NAME" |
15 echo "Usage: $PRG [OPTIONS] NAME" |