equal
deleted
inserted
replaced
9 PRG="$(basename "$0")" |
9 PRG="$(basename "$0")" |
10 |
10 |
11 function usage() |
11 function usage() |
12 { |
12 { |
13 echo |
13 echo |
14 echo "Usage: $PRG [OPTIONS] NAME" |
14 echo "Usage: isabelle $PRG [OPTIONS] NAME" |
15 echo |
15 echo |
16 echo " Create instance NAME of the Isabelle logo (as EPS)." |
16 echo " Create instance NAME of the Isabelle logo (as EPS)." |
17 echo |
17 echo |
18 echo " Options are:" |
18 echo " Options are:" |
19 echo " -o OUTFILE set output file (default determined from NAME)" |
19 echo " -o OUTFILE set output file (default determined from NAME)" |