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;