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