| author | wenzelm |
| Fri, 09 Nov 2001 00:01:55 +0100 | |
| changeset 12111 | d942348d8faf |
| parent 10555 | 2323ec838401 |
| child 13076 | 70704dd48bd5 |
| permissions | -rwxr-xr-x |
1 #!/usr/bin/env bash
2 #
3 # $Id$
4 # Author: Markus Wenzel, TU Muenchen
5 # License: GPL (GNU GENERAL PUBLIC LICENSE)
6 #
7 # feeder - feed isabelle session
10 ## diagnostics
12 PRG="$(basename "$0")"
13 DIR="$(dirname "$0")"
15 function usage()
16 {
17 echo
18 echo "Usage: $PRG [OPTIONS]"
19 echo
20 echo " Options are:"
21 echo " -h TEXT head text"
22 echo " -p emit my pid"
23 echo " -q do not pipe stdin"
24 echo " -t TEXT tail text"
25 echo
26 echo " Output texts (pid, head, stdin, tail), then wait to be terminated."
27 echo
28 exit 1
29 }
31 function fail()
32 {
33 echo "$1" >&2
34 exit 2
35 }
38 ## process command line
40 # options
42 HEAD=""
43 EMITPID=""
44 QUIT=""
45 TAIL=""
47 while getopts "h:pqt:" OPT
48 do
49 case "$OPT" in
50 h)
51 HEAD="$OPTARG"
52 ;;
53 p)
54 EMITPID=true
55 ;;
56 q)
57 QUIT=true
58 ;;
59 t)
60 TAIL="$OPTARG"
61 ;;
62 \?)
63 usage
64 ;;
65 esac
66 done
68 shift $(($OPTIND - 1))
71 # args
73 [ "$#" -ne 0 ] && { echo "Bad args: $*"; usage; }
77 ## main
79 #set by configure
80 AUTO_PERL=perl
82 exec "$AUTO_PERL" -w "$DIR"/feeder.pl "$HEAD" "$EMITPID" "$QUIT" "$TAIL"