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