| Mon, 28 Dec 2009 18:37:11 +0100 | wenzelm | pid without newline -- required for Scala version of system_out; | file | diff | annotate |
| Sat, 20 Dec 2008 11:55:34 +0100 | wenzelm | removed Ids; | file | diff | annotate |
| Thu, 21 Feb 2008 20:16:02 +0100 | wenzelm | removed junk; | file | diff | annotate |
| Tue, 19 Feb 2008 20:34:28 +0100 | wenzelm | replaced setpgrp by more elaborate setsid; | file | diff | annotate |
| Mon, 18 Feb 2008 21:33:29 +0100 | wenzelm | system.pl - invoke shell command line (with robust signal handling); | file | diff | annotate |