| author | blanchet | 
| Tue, 11 Sep 2012 09:40:05 +0200 | |
| changeset 49267 | c96a07255e10 | 
| parent 47868 | 32c03d45fffe | 
| child 61187 | ff00ad5dc03a | 
| permissions | -rw-r--r-- | 
# # Author: Markus Wenzel, TU Muenchen # # feeder.pl - feed isabelle session # # args ($head, $emitpid, $quit, $tail) = @ARGV; # setup signal handlers $SIG{'INT'} = "IGNORE"; # main #buffer lines $| = 1; $emitpid && (print $$, "\n"); if ($head) { utf8::upgrade($head); $head =~ s/([\x80-\xff])/\\${\(ord($1))}/g; print $head, "\n"; } if (!$quit) { while (<STDIN>) { print; } } $tail && (print "$tail", "\n"); # wait forever close STDOUT; sleep;