lib/scripts/process
author wenzelm
Mon Sep 20 23:36:26 2010 +0200 (2010-09-20)
changeset 39576 48baf61cb888
parent 35024 lib/scripts/bash@0faeabd99289
child 39581 430ff865089b
permissions -rwxr-xr-x
refined ML/Scala bash wrapper, based on more general lib/scripts/process;
wenzelm@35023
     1
#!/usr/bin/env perl
wenzelm@26092
     2
#
wenzelm@26092
     3
# Author: Makarius
wenzelm@26092
     4
#
wenzelm@39576
     5
# exec process - with optional process group and report of pid
wenzelm@26092
     6
#
wenzelm@26092
     7
wenzelm@35023
     8
use warnings;
wenzelm@35023
     9
use strict;
wenzelm@35023
    10
wenzelm@26092
    11
# args
wenzelm@26092
    12
wenzelm@39576
    13
my ($group, $pid_name, $cmd_line) = @ARGV;
wenzelm@26092
    14
wenzelm@26092
    15
wenzelm@39576
    16
# process group
wenzelm@26092
    17
wenzelm@26096
    18
if ($group eq "group") {
wenzelm@26096
    19
  use POSIX "setsid";
wenzelm@26107
    20
  POSIX::setsid || die $!;
wenzelm@26096
    21
}
wenzelm@26092
    22
wenzelm@39576
    23
wenzelm@39576
    24
# pid
wenzelm@39576
    25
wenzelm@26092
    26
open (PID_FILE, ">", $pid_name) || die $!;
wenzelm@34197
    27
print PID_FILE "$$";
wenzelm@26092
    28
close PID_FILE;
wenzelm@26092
    29
wenzelm@26092
    30
wenzelm@39576
    31
# exec process
wenzelm@26092
    32
wenzelm@39576
    33
exec "$cmd_line";
wenzelm@39576
    34