lib/scripts/system.pl
changeset 35060 6088dfd5f9c8
parent 35059 acbc346e5310
parent 35054 a5db9779b026
child 35061 be1e25a62ec8
child 35117 eeec2a320a77
--- a/lib/scripts/system.pl	Mon Feb 08 15:49:01 2010 -0800
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,28 +0,0 @@
-#
-# 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 "$$";
-close PID_FILE;
-
-
-# exec script
-
-$SIG{'INT'} = "DEFAULT";   #paranoia setting, required for Cygwin
-exec qq/exec bash '$script_name' > '$output_name'/;
-