lib/scripts/feeder.pl
author ballarin
Tue, 30 Sep 2003 15:10:26 +0200
changeset 14213 7bf882b0a51e
parent 12111 d942348d8faf
child 14981 e73f8140af78
permissions -rw-r--r--
Changed order of prems in finprod_cong. Slight speedup.

#
# $Id$
# Author: Markus Wenzel, TU Muenchen
# License: GPL (GNU GENERAL PUBLIC LICENSE)
#
# feeder.pl - feed isabelle session
#

# args

($head, $emitpid, $quit, $tail) = @ARGV;


# setup signal handlers

sub hangup { exit(0); }
$SIG{'HUP'} = "hangup";
$SIG{'INT'} = "IGNORE";


# main

#buffer lines
$| = 1;


$emitpid && (print $$, "\n");

$head && (print "$head", "\n");

if (!$quit) {
    while (<STDIN>) {
	print;
    }
}

$tail && (print "$tail", "\n");


# wait forever

close STDOUT;
sleep;