diff options
Diffstat (limited to 'stm/workerPool.ml')
| -rw-r--r-- | stm/workerPool.ml | 7 |
1 files changed, 1 insertions, 6 deletions
diff --git a/stm/workerPool.ml b/stm/workerPool.ml index 45c92c3748..fef9300377 100644 --- a/stm/workerPool.ml +++ b/stm/workerPool.ml @@ -72,12 +72,7 @@ let worker_handshake slave_ic slave_oc = exit 1 let locking { lock; pool = p } f = - try - Mutex.lock lock; - let x = f p in - Mutex.unlock lock; - x - with e -> Mutex.unlock lock; raise e + CThread.with_lock lock ~scope:(fun () -> f p) let rec create_worker extra pool priority id = let cancel = ref false in |
