don't remove the child on wait/kill
- important for wait with timout(0) as we may want to try again until the process has realy exited. - make process_release release the process instead
This commit is contained in:
@@ -53,7 +53,9 @@ process_kill(Pid) :-
|
||||
must_be(integer, Pid),
|
||||
'$process_kill'(Pid).
|
||||
|
||||
process_release(Pid) :- process_wait(Pid, _).
|
||||
process_release(Pid) :-
|
||||
process_wait(Pid, _),
|
||||
'$process_release'(Pid).
|
||||
|
||||
|
||||
must_be_known_options(_, _, []).
|
||||
|
||||
Reference in New Issue
Block a user