------- Comment #3 from daney at gcc dot gnu dot org 2007-08-28 16:56 ------- Looking at the current code, it seems that we may have a problem if we destroy() a process that has already exited. The kill(2) man page suggests that ESRCH could result, in which case we would throw an InternalError. Must investigate...
-- http://gcc.gnu.org/bugzilla/show_bug.cgi?id=33218