From 468050a3831cedf63d7dbdb289d5824097bbe1e0 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Thu, 10 Jan 2019 10:54:46 +0100
Subject: [vio] free resources (file descriptors) as soon as a worker ends

---
 stm/vio_checking.ml | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'stm')

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
-- 
cgit v1.2.3