| author | wenzelm |
| Sat, 20 Dec 2008 11:55:34 +0100 | |
| changeset 29145 | b1c6f4563df7 |
| parent 26107 | 4b5e5fc1d11f |
| child 34197 | aecdcaaa8ff3 |
| permissions | -rw-r--r-- |
| 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 |