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 |