diff options
| author | Enrico Tassi | 2016-03-09 16:23:33 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2016-03-09 16:29:01 +0100 |
| commit | cebc677e01c64c4a3f7081f85e37f3b61a112b68 (patch) | |
| tree | aa286631cfb2b89d0d42f7c5b1321033cf497602 /kernel/nativecode.mli | |
| parent | a5ae3b2856e6cc6683652a0abb5a84b9787527c0 (diff) | |
Win: kill unreliable hence do not waitpid after kill -9 (Close #4369)
This commit also completes 74bd95d10b9f4cccb4bd5b855786c444492b201b
Diffstat (limited to 'kernel/nativecode.mli')
0 files changed, 0 insertions, 0 deletions