| changeset 10512 | d34192966cd8 |
| parent 9789 | 7e5e6c47c0b5 |
| child 10555 | 2323ec838401 |
| 10511:efb3428c9879 | 10512:d34192966cd8 |
|---|---|
7 # feeder - feed isabelle session |
7 # feeder - feed isabelle session |
8 |
8 |
9 |
9 |
10 ## diagnostics |
10 ## diagnostics |
11 |
11 |
12 PRG=$(basename "$0") |
12 PRG="$(basename "$0")" |
13 DIR=$(dirname "$0") |
13 DIR="$(dirname "$0")" |
14 |
14 |
15 function usage() |
15 function usage() |
16 { |
16 { |
17 echo |
17 echo |
18 echo "Usage: $PRG [OPTIONS]" |
18 echo "Usage: $PRG [OPTIONS]" |