feeder: treat header as escaped utf8 to allow initial ML text to refer to non-ASCII file/directory names (e.g. "Documents/" on Chinese Ubuntu);
3 # Author: Markus Wenzel, TU Muenchen
5 # feeder - feed isabelle session
10 PRG="$(basename "$0")"
16 echo "Usage: $PRG [OPTIONS]"
19 echo " -h TEXT head text (encoded as utf8)"
20 echo " -p emit my pid"
21 echo " -q do not pipe stdin"
22 echo " -t TEXT tail text"
24 echo " Output texts (pid, head, stdin, tail), then wait to be terminated."
36 ## process command line
45 while getopts "h:pqt:" OPT
66 shift $(($OPTIND - 1))
71 [ "$#" -ne 0 ] && { echo "Bad args: $*"; usage; }
77 exec perl -w "$DIR"/feeder.pl "$HEAD" "$EMITPID" "$QUIT" "$TAIL"