lib/scripts/feeder
changeset 10512 d34192966cd8
parent 9789 7e5e6c47c0b5
child 10555 2323ec838401
equal deleted inserted replaced
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]"