| author | wenzelm |
| Sat, 20 Dec 2008 11:55:34 +0100 | |
| changeset 29145 | b1c6f4563df7 |
| parent 14981 | e73f8140af78 |
| child 39844 | 05daab5782f6 |
| permissions | -rw-r--r-- |
1 #
2 # Author: Markus Wenzel, TU Muenchen
3 #
4 # feeder.pl - feed isabelle session
5 #
7 # args
9 ($head, $emitpid, $quit, $tail) = @ARGV;
12 # setup signal handlers
14 sub hangup { exit(0); }
15 $SIG{'HUP'} = "hangup";
16 $SIG{'INT'} = "IGNORE";
19 # main
21 #buffer lines
22 $| = 1;
25 $emitpid && (print $$, "\n");
27 $head && (print "$head", "\n");
29 if (!$quit) {
30 while (<STDIN>) {
31 print;
32 }
33 }
35 $tail && (print "$tail", "\n");
38 # wait forever
40 close STDOUT;
41 sleep;