| author | wenzelm | 
| Mon, 01 Jun 2009 15:26:00 +0200 | |
| changeset 31327 | ffa5356cc343 | 
| parent 29145 | b1c6f4563df7 | 
| child 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 $!;  | 
| 
 
260cca2e16fa
system.pl - invoke shell command line (with robust signal handling);
 
wenzelm 
parents:  
diff
changeset
 | 
20  | 
print PID_FILE "$$\n";  | 
| 
 
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  |