Admin/makedist
changeset 44152 a07748619f53
parent 43357 07889e32bc58
child 45086 3933a0cbd049
equal deleted inserted replaced
44151:e842a2cf923c 44152:a07748619f53
    13 
    13 
    14 
    14 
    15 ## diagnostics
    15 ## diagnostics
    16 
    16 
    17 PRG="$(basename "$0")"
    17 PRG="$(basename "$0")"
    18 THIS="$(cd $(dirname "$0"); echo "$PWD")"
    18 THIS="$(cd $(dirname "$0"); pwd)"
    19 
    19 
    20 function usage()
    20 function usage()
    21 {
    21 {
    22   cat <<EOF
    22   cat <<EOF
    23 
    23