lib/scripts/bash
author wenzelm
Sun, 25 Apr 2010 23:09:32 +0200
changeset 36330 0584e203960e
parent 35024 0faeabd99289
permissions -rwxr-xr-x
renamed Drule.unconstrainTs to Thm.unconstrain_allTs to accomdate the version by krauss/schropp; less pervasive names;

#!/usr/bin/env perl
#
# Author: Makarius
#
# bash - invoke shell command line (with robust signal handling)
#

use warnings;
use strict;


# args

my ($group, $script_name, $pid_name, $output_name) = @ARGV;


# process id

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

open (PID_FILE, ">", $pid_name) || die $!;
print PID_FILE "$$";
close PID_FILE;


# exec script

exec qq/exec bash '$script_name' > '$output_name'/;