lib/scripts/system.pl
author nipkow
Wed Aug 26 19:54:19 2009 +0200 (2009-08-26)
changeset 32416 4ea7648b6ae2
parent 29145 b1c6f4563df7
child 34197 aecdcaaa8ff3
permissions -rw-r--r--
merged
     1 #
     2 # Author: Makarius
     3 #
     4 # system.pl - invoke shell command line (with robust signal handling)
     5 #
     6 
     7 # args
     8 
     9 ($group, $script_name, $pid_name, $output_name) = @ARGV;
    10 
    11 
    12 # process id
    13 
    14 if ($group eq "group") {
    15   use POSIX "setsid";
    16   POSIX::setsid || die $!;
    17 }
    18 
    19 open (PID_FILE, ">", $pid_name) || die $!;
    20 print PID_FILE "$$\n";
    21 close PID_FILE;
    22 
    23 
    24 # exec script
    25 
    26 $SIG{'INT'} = "DEFAULT";   #paranoia setting, required for Cygwin
    27 exec qq/exec bash '$script_name' > '$output_name'/;
    28