summaryrefslogtreecommitdiff
path: root/stm/asyncTaskQueue.ml
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <gareuselesinge@debian.org>2015-07-15 10:36:12 +0200
committerGravatar Enrico Tassi <gareuselesinge@debian.org>2015-07-15 10:36:12 +0200
commit0aa2544d04dbd4b6ee665b551ed165e4fb02d2fa (patch)
tree12e8931a4a56da1a1bdfb89d670f4ba38fe08e1f /stm/asyncTaskQueue.ml
parentcec4741afacd2e80894232850eaf9f9c0e45d6d7 (diff)
Imported Upstream version 8.5~beta2+dfsgupstream/8.5_beta2+dfsg
Diffstat (limited to 'stm/asyncTaskQueue.ml')
-rw-r--r--stm/asyncTaskQueue.ml4
1 files changed, 3 insertions, 1 deletions
diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml
index 672527d9..e3fb0b60 100644
--- a/stm/asyncTaskQueue.ml
+++ b/stm/asyncTaskQueue.ml
@@ -177,7 +177,7 @@ module Make(T : Task) = struct
if not (Worker.is_alive proc) then ()
else if cancelled () || !(!expiration_date) then
let () = stop_waiting := true in
- let () = TQueue.signal_destruction queue in
+ let () = TQueue.broadcast queue in
Worker.kill proc
else
let () = Unix.sleep 1 in
@@ -253,6 +253,8 @@ module Make(T : Task) = struct
Pool.destroy active;
TQueue.destroy queue
+ let broadcast { queue } = TQueue.broadcast queue
+
let enqueue_task { queue; active } (t, _ as item) =
prerr_endline ("Enqueue task "^T.name_of_task t);
TQueue.push queue item