aboutsummaryrefslogtreecommitdiffhomepage
path: root/stm
diff options
context:
space:
mode:
Diffstat (limited to 'stm')
-rw-r--r--stm/asyncTaskQueue.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml
index 3cb6e7022..917de9b52 100644
--- a/stm/asyncTaskQueue.ml
+++ b/stm/asyncTaskQueue.ml
@@ -146,6 +146,7 @@ module Make(T : Task) = struct
let manager cpanel (id, proc, ic, oc) =
let { WorkerPool.extra = queue; exit; cancelled } = cpanel in
+ let exit () = report_status ~id "Dead"; exit () in
let last_task = ref None in
let worker_age = ref `Fresh in
let got_token = ref false in