Admin/bash_process/bash_process.c
Wed, 09 Mar 2016 20:11:25 +0100 wenzelm ignore SIGINT in waiting wrapper process;
Wed, 09 Mar 2016 14:24:16 +0100 wenzelm elapsed time in milliseconds (cf. Time.now in Poly/ML);
Wed, 09 Mar 2016 13:33:21 +0100 wenzelm support for timing of the managed process;
Sat, 13 Feb 2016 22:52:41 +0100 wenzelm actually wait for forked process and return its status -- this is not meant to be a daemon;
Sat, 13 Feb 2016 17:27:23 +0100 wenzelm clarified name;
less more (0) tip