| author | wenzelm |
| Sat, 20 Dec 2008 11:55:34 +0100 | |
| changeset 29145 | b1c6f4563df7 |
| parent 26576 | fc76b7b79ba9 |
| child 40597 | 3e4bb6e7c3ca |
| permissions | -rwxr-xr-x |
1 #!/usr/bin/env bash
2 #
3 # Author: Markus Wenzel, TU Muenchen
4 #
5 # feeder - feed isabelle session
8 ## diagnostics
10 PRG="$(basename "$0")"
11 DIR="$(dirname "$0")"
13 function usage()
14 {
15 echo
16 echo "Usage: $PRG [OPTIONS]"
17 echo
18 echo " Options are:"
19 echo " -h TEXT head text"
20 echo " -p emit my pid"
21 echo " -q do not pipe stdin"
22 echo " -t TEXT tail text"
23 echo
24 echo " Output texts (pid, head, stdin, tail), then wait to be terminated."
25 echo
26 exit 1
27 }
29 function fail()
30 {
31 echo "$1" >&2
32 exit 2
33 }
36 ## process command line
38 # options
40 HEAD=""
41 EMITPID=""
42 QUIT=""
43 TAIL=""
45 while getopts "h:pqt:" OPT
46 do
47 case "$OPT" in
48 h)
49 HEAD="$OPTARG"
50 ;;
51 p)
52 EMITPID=true
53 ;;
54 q)
55 QUIT=true
56 ;;
57 t)
58 TAIL="$OPTARG"
59 ;;
60 \?)
61 usage
62 ;;
63 esac
64 done
66 shift $(($OPTIND - 1))
69 # args
71 [ "$#" -ne 0 ] && { echo "Bad args: $*"; usage; }
75 ## main
77 exec perl -w "$DIR"/feeder.pl "$HEAD" "$EMITPID" "$QUIT" "$TAIL"