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