Mercurial Mercurial > repos > isabelle / annotate
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
lib/scripts/process
author wenzelm
Mon, 20 Sep 2010 23:36:26 +0200
changeset 39576 48baf61cb888
parent 35024 lib/scripts/bash@0faeabd99289
child 39581 430ff865089b
permissions -rwxr-xr-x
refined ML/Scala bash wrapper, based on more general lib/scripts/process;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
35023
16f9877abf0b modernized perl scripts: prefer standalone executables;
wenzelm
parents: 34197
diff changeset 
     1
 
#!/usr/bin/env perl
26092
260cca2e16fa system.pl - invoke shell command line (with robust signal handling);
wenzelm
parents:
diff changeset 
     2
 
#
260cca2e16fa system.pl - invoke shell command line (with robust signal handling);
wenzelm
parents:
diff changeset 
     3
 
# Author: Makarius
260cca2e16fa system.pl - invoke shell command line (with robust signal handling);
wenzelm
parents:
diff changeset 
     4
 
#
39576
48baf61cb888 refined ML/Scala bash wrapper, based on more general lib/scripts/process;
wenzelm
parents: 35024
diff changeset 
     5
 
# exec process - with optional process group and report of pid
26092
260cca2e16fa system.pl - invoke shell command line (with robust signal handling);
wenzelm
parents:
diff changeset 
     6
 
#
260cca2e16fa system.pl - invoke shell command line (with robust signal handling);
wenzelm
parents:
diff changeset 
     7
 







35023






16f9877abf0b
modernized perl scripts: prefer standalone executables;



wenzelm


parents: 
34197

diff
changeset




     8


use warnings;













16f9877abf0b
modernized perl scripts: prefer standalone executables;



wenzelm


parents: 
34197

diff
changeset




     9


use strict;













16f9877abf0b
modernized perl scripts: prefer standalone executables;



wenzelm


parents: 
34197

diff
changeset




    10









26092






260cca2e16fa
system.pl - invoke shell command line (with robust signal handling);



wenzelm


parents: 

diff
changeset




    11


# args













260cca2e16fa
system.pl - invoke shell command line (with robust signal handling);



wenzelm


parents: 

diff
changeset




    12









39576






48baf61cb888
refined ML/Scala bash wrapper, based on more general lib/scripts/process;



wenzelm


parents: 
35024

diff
changeset




    13


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








26092






260cca2e16fa
system.pl - invoke shell command line (with robust signal handling);



wenzelm


parents: 

diff
changeset




    14














260cca2e16fa
system.pl - invoke shell command line (with robust signal handling);



wenzelm


parents: 

diff
changeset




    15









39576






48baf61cb888
refined ML/Scala bash wrapper, based on more general lib/scripts/process;



wenzelm


parents: 
35024

diff
changeset




    16


# process group








26092






260cca2e16fa
system.pl - invoke shell command line (with robust signal handling);



wenzelm


parents: 

diff
changeset




    17









26096






783f957dcb01
replaced setpgrp by more elaborate setsid;



wenzelm


parents: 
26092

diff
changeset




    18


if ($group eq "group") {













783f957dcb01
replaced setpgrp by more elaborate setsid;



wenzelm


parents: 
26092

diff
changeset




    19


  use POSIX "setsid";








26107






4b5e5fc1d11f
removed junk;



wenzelm


parents: 
26096

diff
changeset




    20


  POSIX::setsid || die $!;








26096






783f957dcb01
replaced setpgrp by more elaborate setsid;



wenzelm


parents: 
26092

diff
changeset




    21


}








26092






260cca2e16fa
system.pl - invoke shell command line (with robust signal handling);



wenzelm


parents: 

diff
changeset




    22









39576






48baf61cb888
refined ML/Scala bash wrapper, based on more general lib/scripts/process;



wenzelm


parents: 
35024

diff
changeset




    23














48baf61cb888
refined ML/Scala bash wrapper, based on more general lib/scripts/process;



wenzelm


parents: 
35024

diff
changeset




    24


# pid













48baf61cb888
refined ML/Scala bash wrapper, based on more general lib/scripts/process;



wenzelm


parents: 
35024

diff
changeset




    25









26092






260cca2e16fa
system.pl - invoke shell command line (with robust signal handling);



wenzelm


parents: 

diff
changeset




    26


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








34197






aecdcaaa8ff3
pid without newline -- required for Scala version of system_out;



wenzelm


parents: 
29145

diff
changeset




    27


print PID_FILE "$$";








26092






260cca2e16fa
system.pl - invoke shell command line (with robust signal handling);



wenzelm


parents: 

diff
changeset




    28


close PID_FILE;













260cca2e16fa
system.pl - invoke shell command line (with robust signal handling);



wenzelm


parents: 

diff
changeset




    29














260cca2e16fa
system.pl - invoke shell command line (with robust signal handling);



wenzelm


parents: 

diff
changeset




    30









39576






48baf61cb888
refined ML/Scala bash wrapper, based on more general lib/scripts/process;



wenzelm


parents: 
35024

diff
changeset




    31


# exec process








26092






260cca2e16fa
system.pl - invoke shell command line (with robust signal handling);



wenzelm


parents: 

diff
changeset




    32









39576






48baf61cb888
refined ML/Scala bash wrapper, based on more general lib/scripts/process;



wenzelm


parents: 
35024

diff
changeset




    33


exec "$cmd_line";













48baf61cb888
refined ML/Scala bash wrapper, based on more general lib/scripts/process;



wenzelm


parents: 
35024

diff
changeset




    34
















isabelle