| author | paulson |
| Tue, 02 Feb 2010 09:48:20 +0000 | |
| changeset 35503 | 7bba12c3b7b6 |
| parent 34197 | aecdcaaa8ff3 |
| 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 |
# Author: Makarius |
|
260cca2e16fa
system.pl - invoke shell command line (with robust signal handling);
wenzelm
parents:
diff
changeset
|
3 |
# |
|
260cca2e16fa
system.pl - invoke shell command line (with robust signal handling);
wenzelm
parents:
diff
changeset
|
4 |
# 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
|
5 |
# |
|
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 |
# args |
|
260cca2e16fa
system.pl - invoke shell command line (with robust signal handling);
wenzelm
parents:
diff
changeset
|
8 |
|
|
260cca2e16fa
system.pl - invoke shell command line (with robust signal handling);
wenzelm
parents:
diff
changeset
|
9 |
($group, $script_name, $pid_name, $output_name) = @ARGV; |
|
260cca2e16fa
system.pl - invoke shell command line (with robust signal handling);
wenzelm
parents:
diff
changeset
|
10 |
|
|
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 |
# process id |
|
260cca2e16fa
system.pl - invoke shell command line (with robust signal handling);
wenzelm
parents:
diff
changeset
|
13 |
|
| 26096 | 14 |
if ($group eq "group") {
|
15 |
use POSIX "setsid"; |
|
| 26107 | 16 |
POSIX::setsid || die $!; |
| 26096 | 17 |
} |
|
26092
260cca2e16fa
system.pl - invoke shell command line (with robust signal handling);
wenzelm
parents:
diff
changeset
|
18 |
|
|
260cca2e16fa
system.pl - invoke shell command line (with robust signal handling);
wenzelm
parents:
diff
changeset
|
19 |
open (PID_FILE, ">", $pid_name) || die $!; |
|
34197
aecdcaaa8ff3
pid without newline -- required for Scala version of system_out;
wenzelm
parents:
29145
diff
changeset
|
20 |
print PID_FILE "$$"; |
|
26092
260cca2e16fa
system.pl - invoke shell command line (with robust signal handling);
wenzelm
parents:
diff
changeset
|
21 |
close PID_FILE; |
|
260cca2e16fa
system.pl - invoke shell command line (with robust signal handling);
wenzelm
parents:
diff
changeset
|
22 |
|
|
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 |
# exec script |
|
260cca2e16fa
system.pl - invoke shell command line (with robust signal handling);
wenzelm
parents:
diff
changeset
|
25 |
|
|
260cca2e16fa
system.pl - invoke shell command line (with robust signal handling);
wenzelm
parents:
diff
changeset
|
26 |
$SIG{'INT'} = "DEFAULT"; #paranoia setting, required for Cygwin
|
|
260cca2e16fa
system.pl - invoke shell command line (with robust signal handling);
wenzelm
parents:
diff
changeset
|
27 |
exec qq/exec bash '$script_name' > '$output_name'/; |
|
260cca2e16fa
system.pl - invoke shell command line (with robust signal handling);
wenzelm
parents:
diff
changeset
|
28 |