lib/scripts/system.pl
changeset 35023 16f9877abf0b
parent 35022 c844b93dd147
child 35024 0faeabd99289
equal deleted inserted replaced
35022:c844b93dd147 35023:16f9877abf0b
     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 "$$";
       
    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