[vio] free resources (file descriptors) as soon as a worker ends

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