lib/scripts/bash
author wenzelm
Thu May 20 20:20:52 2010 +0200 (2010-05-20)
changeset 37012 106c56e916f8
parent 35024 0faeabd99289
permissions -rwxr-xr-x
enable shell script editor mode;
wenzelm@35023
     1
#!/usr/bin/env perl
wenzelm@26092
     2
#
wenzelm@26092
     3
# Author: Makarius
wenzelm@26092
     4
#
wenzelm@35023
     5
# bash - invoke shell command line (with robust signal handling)
wenzelm@26092
     6
#
wenzelm@26092
     7
wenzelm@35023
     8
use warnings;
wenzelm@35023
     9
use strict;
wenzelm@35023
    10
wenzelm@35023
    11
wenzelm@26092
    12
# args
wenzelm@26092
    13
wenzelm@35023
    14
my ($group, $script_name, $pid_name, $output_name) = @ARGV;
wenzelm@26092
    15
wenzelm@26092
    16
wenzelm@26092
    17
# process id
wenzelm@26092
    18
wenzelm@26096
    19
if ($group eq "group") {
wenzelm@26096
    20
  use POSIX "setsid";
wenzelm@26107
    21
  POSIX::setsid || die $!;
wenzelm@26096
    22
}
wenzelm@26092
    23
wenzelm@26092
    24
open (PID_FILE, ">", $pid_name) || die $!;
wenzelm@34197
    25
print PID_FILE "$$";
wenzelm@26092
    26
close PID_FILE;
wenzelm@26092
    27
wenzelm@26092
    28
wenzelm@26092
    29
# exec script
wenzelm@26092
    30
wenzelm@26092
    31
exec qq/exec bash '$script_name' > '$output_name'/;