diff options
Diffstat (limited to 'stm/vio_checking.ml')
| -rw-r--r-- | stm/vio_checking.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/stm/vio_checking.ml b/stm/vio_checking.ml index 64f19e1fd9..41e11ba255 100644 --- a/stm/vio_checking.ml +++ b/stm/vio_checking.ml @@ -95,6 +95,7 @@ let schedule_vio_checking j fs = done; let pid, ret = Unix.wait () in if ret <> Unix.WEXITED 0 then rc := 1; + Worker.kill (Pool.find pid !pool); pool := Pool.remove pid !pool; done; exit !rc @@ -137,6 +138,7 @@ let schedule_vio_compilation j fs = done; let pid, ret = Unix.wait () in if ret <> Unix.WEXITED 0 then rc := 1; + Worker.kill (Pool.find pid !pool); pool := Pool.remove pid !pool; done; exit !rc |