1. 2018-07-06 [4] [Bug-dejagnu] close_wait_program, process groups and kill /bin/sh builti dejagnu-bug Ben Elliston