lib/scripts/system.pl
author wenzelm
Thu, 21 Aug 2008 13:05:28 +0200
changeset 27934 7d12a7e3cc55
parent 26107 4b5e5fc1d11f
child 29145 b1c6f4563df7
permissions -rw-r--r--
added ISABELLE_ROOT_JVM; removed obsolete ISABELLE_HOME_JVM, ISABELLE_HOME_USER_JVM;

#
# $Id$
# Author: Makarius
#
# system.pl - invoke shell command line (with robust signal handling)
#

# args

($group, $script_name, $pid_name, $output_name) = @ARGV;


# process id

if ($group eq "group") {
  use POSIX "setsid";
  POSIX::setsid || die $!;
}

open (PID_FILE, ">", $pid_name) || die $!;
print PID_FILE "$$\n";
close PID_FILE;


# exec script

$SIG{'INT'} = "DEFAULT";   #paranoia setting, required for Cygwin
exec qq/exec bash '$script_name' > '$output_name'/;