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