aboutsummaryrefslogtreecommitdiffhomepage
path: root/stm
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2014-12-17 20:25:06 +0100
committerGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2014-12-17 20:25:18 +0100
commitc6d356844ec857b376302c50c925faae558814a9 (patch)
treec6bbfa093852b5e4bc383ed84c534e22b0983d29 /stm
parent7ebe6117789ac3c0d31c8a6ed918fce71b6d2e4b (diff)
Fix compilation with ocaml 4.0.0
Diffstat (limited to 'stm')
-rw-r--r--stm/workerPool.ml12
1 files changed, 6 insertions, 6 deletions
diff --git a/stm/workerPool.ml b/stm/workerPool.ml
index 4757760c7..ee3809488 100644
--- a/stm/workerPool.ml
+++ b/stm/workerPool.ml
@@ -37,7 +37,7 @@ type worker = {
type pre_pool = {
workers : worker list ref;
count : int ref;
- extra : Model.extra;
+ extra_arg : Model.extra;
}
type pool = { lock : Mutex.t; pool : pre_pool }
@@ -87,10 +87,10 @@ let rec create_worker extra pool id =
let manager = Thread.create (Model.manager cpanel) worker in
{ name; cancel; manager; process }
-and cleanup x = locking x begin fun { workers; count; extra } ->
+and cleanup x = locking x begin fun { workers; count; extra_arg } ->
workers := List.map (function
| { cancel } as w when !cancel = false -> w
- | _ -> let n = !count in incr count; create_worker extra x n)
+ | _ -> let n = !count in incr count; create_worker extra_arg x n)
!workers
end
@@ -100,15 +100,15 @@ end
let is_empty x = locking x begin fun { workers } -> !workers = [] end
-let create extra ~size = let x = {
+let create extra_arg ~size = let x = {
lock = Mutex.create ();
pool = {
- extra;
+ extra_arg;
workers = ref [];
count = ref size;
}} in
locking x begin fun { workers } ->
- workers := CList.init size (create_worker extra x)
+ workers := CList.init size (create_worker extra_arg x)
end;
x