lib/scripts/process
author blanchet
Thu, 24 Jul 2014 00:24:00 +0200
changeset 57629 e88b5f59cade
parent 39583 c1e9c6dfeff8
permissions -rwxr-xr-x
use the noted theorem whenever possible, because it has a named derivation (leading to cleaner proof terms)

#!/usr/bin/env perl
#
# Author: Makarius
#
# exec process - with optional process group and report of pid
#

use warnings;
use strict;

# process group

my $group = $ARGV[0]; shift(@ARGV);

if ($group eq "group") {
  use POSIX "setsid";
  POSIX::setsid || die $!;
}


# report pid

my $pid_name = $ARGV[0]; shift(@ARGV);

if ($pid_name eq "-") {
  print "$$\n";
}
else {
  open (PID_FILE, ">", $pid_name) || die $!;
  print PID_FILE "$$";
  close PID_FILE;
}


# exec process

my $script = $ARGV[0]; shift(@ARGV);

if ($script eq "script") {
  my $cmd_line = $ARGV[0]; shift(@ARGV);
  exec $cmd_line || die $!;
}
else {
  (exec { $ARGV[0] } @ARGV) || die $!;
}