lib/scripts/bash
changeset 35023 16f9877abf0b
parent 34197 aecdcaaa8ff3
child 35024 0faeabd99289
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/scripts/bash	Sun Feb 07 20:21:38 2010 +0100
@@ -0,0 +1,32 @@
+#!/usr/bin/env perl
+#
+# Author: Makarius
+#
+# bash - invoke shell command line (with robust signal handling)
+#
+
+use warnings;
+use strict;
+
+
+# args
+
+my ($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'/;