lib/scripts/process
author wenzelm
Tue, 21 Sep 2010 22:16:22 +0200
changeset 39581 430ff865089b
parent 39576 48baf61cb888
child 39583 c1e9c6dfeff8
permissions -rwxr-xr-x
refined Isabelle_System.bash_output: pass pid via stdout, separate stdout/stderr;

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

use warnings;
use strict;

# args

my ($group, $pid_name, $cmd_line) = @ARGV;


# process group

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


# pid

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


# exec process

exec $cmd_line;