lib/scripts/system.pl
author huffman
Fri, 20 Jun 2008 19:59:00 +0200
changeset 27296 eec7a1889ca5
parent 26107 4b5e5fc1d11f
child 29145 b1c6f4563df7
permissions -rw-r--r--
moved Abs_image to Typedef.thy; prove finite_UNIV outside the locale
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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
783f957dcb01 replaced setpgrp by more elaborate setsid;
wenzelm
parents: 26092
diff changeset
    15
if ($group eq "group") {
783f957dcb01 replaced setpgrp by more elaborate setsid;
wenzelm
parents: 26092
diff changeset
    16
  use POSIX "setsid";
26107
4b5e5fc1d11f removed junk;
wenzelm
parents: 26096
diff changeset
    17
  POSIX::setsid || die $!;
26096
783f957dcb01 replaced setpgrp by more elaborate setsid;
wenzelm
parents: 26092
diff changeset
    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