author | nipkow |
Tue, 18 Sep 2012 03:33:53 +0200 | |
changeset 49433 | 1095f240146a |
parent 39583 | c1e9c6dfeff8 |
permissions | -rwxr-xr-x |
35023
16f9877abf0b
modernized perl scripts: prefer standalone executables;
wenzelm
parents:
34197
diff
changeset
|
1 |
#!/usr/bin/env perl |
26092
260cca2e16fa
system.pl - invoke shell command line (with robust signal handling);
wenzelm
parents:
diff
changeset
|
2 |
# |
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 |
# |
39576
48baf61cb888
refined ML/Scala bash wrapper, based on more general lib/scripts/process;
wenzelm
parents:
35024
diff
changeset
|
5 |
# exec process - with optional process group and report of pid |
26092
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 |
|
35023
16f9877abf0b
modernized perl scripts: prefer standalone executables;
wenzelm
parents:
34197
diff
changeset
|
8 |
use warnings; |
16f9877abf0b
modernized perl scripts: prefer standalone executables;
wenzelm
parents:
34197
diff
changeset
|
9 |
use strict; |
16f9877abf0b
modernized perl scripts: prefer standalone executables;
wenzelm
parents:
34197
diff
changeset
|
10 |
|
39583
c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents:
39581
diff
changeset
|
11 |
# process group |
26092
260cca2e16fa
system.pl - invoke shell command line (with robust signal handling);
wenzelm
parents:
diff
changeset
|
12 |
|
39583
c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents:
39581
diff
changeset
|
13 |
my $group = $ARGV[0]; shift(@ARGV); |
26092
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 |
|
39576
48baf61cb888
refined ML/Scala bash wrapper, based on more general lib/scripts/process;
wenzelm
parents:
35024
diff
changeset
|
20 |
|
39583
c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents:
39581
diff
changeset
|
21 |
# report pid |
c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents:
39581
diff
changeset
|
22 |
|
c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents:
39581
diff
changeset
|
23 |
my $pid_name = $ARGV[0]; shift(@ARGV); |
39576
48baf61cb888
refined ML/Scala bash wrapper, based on more general lib/scripts/process;
wenzelm
parents:
35024
diff
changeset
|
24 |
|
39581
430ff865089b
refined Isabelle_System.bash_output: pass pid via stdout, separate stdout/stderr;
wenzelm
parents:
39576
diff
changeset
|
25 |
if ($pid_name eq "-") { |
430ff865089b
refined Isabelle_System.bash_output: pass pid via stdout, separate stdout/stderr;
wenzelm
parents:
39576
diff
changeset
|
26 |
print "$$\n"; |
430ff865089b
refined Isabelle_System.bash_output: pass pid via stdout, separate stdout/stderr;
wenzelm
parents:
39576
diff
changeset
|
27 |
} |
430ff865089b
refined Isabelle_System.bash_output: pass pid via stdout, separate stdout/stderr;
wenzelm
parents:
39576
diff
changeset
|
28 |
else { |
430ff865089b
refined Isabelle_System.bash_output: pass pid via stdout, separate stdout/stderr;
wenzelm
parents:
39576
diff
changeset
|
29 |
open (PID_FILE, ">", $pid_name) || die $!; |
430ff865089b
refined Isabelle_System.bash_output: pass pid via stdout, separate stdout/stderr;
wenzelm
parents:
39576
diff
changeset
|
30 |
print PID_FILE "$$"; |
430ff865089b
refined Isabelle_System.bash_output: pass pid via stdout, separate stdout/stderr;
wenzelm
parents:
39576
diff
changeset
|
31 |
close PID_FILE; |
430ff865089b
refined Isabelle_System.bash_output: pass pid via stdout, separate stdout/stderr;
wenzelm
parents:
39576
diff
changeset
|
32 |
} |
26092
260cca2e16fa
system.pl - invoke shell command line (with robust signal handling);
wenzelm
parents:
diff
changeset
|
33 |
|
260cca2e16fa
system.pl - invoke shell command line (with robust signal handling);
wenzelm
parents:
diff
changeset
|
34 |
|
39576
48baf61cb888
refined ML/Scala bash wrapper, based on more general lib/scripts/process;
wenzelm
parents:
35024
diff
changeset
|
35 |
# exec process |
26092
260cca2e16fa
system.pl - invoke shell command line (with robust signal handling);
wenzelm
parents:
diff
changeset
|
36 |
|
39583
c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents:
39581
diff
changeset
|
37 |
my $script = $ARGV[0]; shift(@ARGV); |
39576
48baf61cb888
refined ML/Scala bash wrapper, based on more general lib/scripts/process;
wenzelm
parents:
35024
diff
changeset
|
38 |
|
39583
c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents:
39581
diff
changeset
|
39 |
if ($script eq "script") { |
c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents:
39581
diff
changeset
|
40 |
my $cmd_line = $ARGV[0]; shift(@ARGV); |
c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents:
39581
diff
changeset
|
41 |
exec $cmd_line || die $!; |
c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents:
39581
diff
changeset
|
42 |
} |
c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents:
39581
diff
changeset
|
43 |
else { |
c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents:
39581
diff
changeset
|
44 |
(exec { $ARGV[0] } @ARGV) || die $!; |
c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents:
39581
diff
changeset
|
45 |
} |
c1e9c6dfeff8
more robust lib/scripts/process, with explicit script/no_script mode;
wenzelm
parents:
39581
diff
changeset
|
46 |