lib/scripts/bash
changeset 35023 16f9877abf0b
parent 34197 aecdcaaa8ff3
child 35024 0faeabd99289
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/lib/scripts/bash	Sun Feb 07 20:21:38 2010 +0100
     1.3 @@ -0,0 +1,32 @@
     1.4 +#!/usr/bin/env perl
     1.5 +#
     1.6 +# Author: Makarius
     1.7 +#
     1.8 +# bash - invoke shell command line (with robust signal handling)
     1.9 +#
    1.10 +
    1.11 +use warnings;
    1.12 +use strict;
    1.13 +
    1.14 +
    1.15 +# args
    1.16 +
    1.17 +my ($group, $script_name, $pid_name, $output_name) = @ARGV;
    1.18 +
    1.19 +
    1.20 +# process id
    1.21 +
    1.22 +if ($group eq "group") {
    1.23 +  use POSIX "setsid";
    1.24 +  POSIX::setsid || die $!;
    1.25 +}
    1.26 +
    1.27 +open (PID_FILE, ">", $pid_name) || die $!;
    1.28 +print PID_FILE "$$";
    1.29 +close PID_FILE;
    1.30 +
    1.31 +
    1.32 +# exec script
    1.33 +
    1.34 +$SIG{'INT'} = "DEFAULT";   #paranoia setting, required for Cygwin
    1.35 +exec qq/exec bash '$script_name' > '$output_name'/;