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