| author | bulwahn |
| Wed, 10 Oct 2012 10:48:55 +0200 | |
| changeset 49768 | 3ecfba7e731d |
| parent 40335 | 3e4bb6e7c3ca |
| permissions | -rwxr-xr-x |
#!/usr/bin/env bash # # Author: Markus Wenzel, TU Muenchen # # feeder - feed isabelle session ## diagnostics PRG="$(basename "$0")" DIR="$(dirname "$0")" function usage() { echo echo "Usage: $PRG [OPTIONS]" echo echo " Options are:" echo " -h TEXT head text (encoded as utf8)" echo " -p emit my pid" echo " -q do not pipe stdin" echo " -t TEXT tail text" echo echo " Output texts (pid, head, stdin, tail), then wait to be terminated." echo exit 1 } function fail() { echo "$1" >&2 exit 2 } ## process command line # options HEAD="" EMITPID="" QUIT="" TAIL="" while getopts "h:pqt:" OPT do case "$OPT" in h) HEAD="$OPTARG" ;; p) EMITPID=true ;; q) QUIT=true ;; t) TAIL="$OPTARG" ;; \?) usage ;; esac done shift $(($OPTIND - 1)) # args [ "$#" -ne 0 ] && { echo "Bad args: $*"; usage; } ## main exec perl -w "$DIR"/feeder.pl "$HEAD" "$EMITPID" "$QUIT" "$TAIL"