diff options
| author | coqbot-app[bot] | 2021-04-12 12:34:16 +0000 |
|---|---|---|
| committer | GitHub | 2021-04-12 12:34:16 +0000 |
| commit | 271445decd0fc1a37da3009f148f2e68c7168fe1 (patch) | |
| tree | 631d9976d17d6573b0f348cfd6fdbd83bb779ddb /lib/future.ml | |
| parent | 7ce1c4844b077adb25d14cf1bbd2d22548b1e935 (diff) | |
| parent | 520ac61dfe5a6e865cb7b10f4a822c0d72f3ded9 (diff) | |
Merge PR #14046: make critical sections safe in the presence of exceptions
Reviewed-by: ejgallego
Ack-by: gares
Ack-by: SkySkimmer
Ack-by: gadmm
Diffstat (limited to 'lib/future.ml')
| -rw-r--r-- | lib/future.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/lib/future.ml b/lib/future.ml index 23d089fb6b..247b139798 100644 --- a/lib/future.ml +++ b/lib/future.ml @@ -112,8 +112,8 @@ let create_delegate ?(blocking=true) ~name fix_exn = if not blocking then (fun () -> raise (NotReady name)), ignore else let lock = Mutex.create () in let cond = Condition.create () in - (fun () -> Mutex.lock lock; Condition.wait cond lock; Mutex.unlock lock), - (fun () -> Mutex.lock lock; Condition.broadcast cond; Mutex.unlock lock) in + (fun () -> CThread.with_lock lock ~scope:(fun () -> Condition.wait cond lock)), + (fun () -> CThread.with_lock lock ~scope:(fun () -> Condition.broadcast cond)) in let ck = create ~name ~fix_exn (Delegated wait) in ck, assignment signal ck |
