diff options
author | Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-12-17 20:25:06 +0100 |
---|---|---|
committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-12-17 20:25:18 +0100 |
commit | c6d356844ec857b376302c50c925faae558814a9 (patch) | |
tree | c6bbfa093852b5e4bc383ed84c534e22b0983d29 /stm | |
parent | 7ebe6117789ac3c0d31c8a6ed918fce71b6d2e4b (diff) |
Fix compilation with ocaml 4.0.0
Diffstat (limited to 'stm')
-rw-r--r-- | stm/workerPool.ml | 12 |
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 |