lib/scripts/process
author wenzelm
Thu Nov 13 23:45:15 2014 +0100 (2014-11-13)
changeset 58999 ed09ae4ea2d8
parent 39583 c1e9c6dfeff8
permissions -rwxr-xr-x
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
discontinued obsolete 'txt_raw' (superseded by 'text_raw');
eliminated obsolete Outer_Syntax.markup (superseded by keyword kinds);
'text' and 'txt' no longer appear in Sidekick tree due to change of keyword kind;
changed tagging of diagnostic commands within proof;
     1 #!/usr/bin/env perl
     2 #
     3 # Author: Makarius
     4 #
     5 # exec process - with optional process group and report of pid
     6 #
     7 
     8 use warnings;
     9 use strict;
    10 
    11 # process group
    12 
    13 my $group = $ARGV[0]; shift(@ARGV);
    14 
    15 if ($group eq "group") {
    16   use POSIX "setsid";
    17   POSIX::setsid || die $!;
    18 }
    19 
    20 
    21 # report pid
    22 
    23 my $pid_name = $ARGV[0]; shift(@ARGV);
    24 
    25 if ($pid_name eq "-") {
    26   print "$$\n";
    27 }
    28 else {
    29   open (PID_FILE, ">", $pid_name) || die $!;
    30   print PID_FILE "$$";
    31   close PID_FILE;
    32 }
    33 
    34 
    35 # exec process
    36 
    37 my $script = $ARGV[0]; shift(@ARGV);
    38 
    39 if ($script eq "script") {
    40   my $cmd_line = $ARGV[0]; shift(@ARGV);
    41   exec $cmd_line || die $!;
    42 }
    43 else {
    44   (exec { $ARGV[0] } @ARGV) || die $!;
    45 }
    46