equal
deleted
inserted
replaced
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 [OPTIONS] [VARNAMES ...]" |
16 echo "Usage: isabelle $PRG [OPTIONS] [VARNAMES ...]" |
17 echo |
17 echo |
18 echo " Options are:" |
18 echo " Options are:" |
19 echo " -a display complete environment" |
19 echo " -a display complete environment" |
20 echo " -b print values only (doesn't work for -a)" |
20 echo " -b print values only (doesn't work for -a)" |
21 echo |
21 echo |