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 /clib/cThread.mli | |
| 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 'clib/cThread.mli')
| -rw-r--r-- | clib/cThread.mli | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/clib/cThread.mli b/clib/cThread.mli index 87889f3356..d974135d43 100644 --- a/clib/cThread.mli +++ b/clib/cThread.mli @@ -29,3 +29,8 @@ val thread_friendly_really_read_line : thread_ic -> string (* Wrapper around Thread.create that blocks signals such as Sys.sigalrm (used * for Timeout *) val create : ('a -> 'b) -> 'a -> Thread.t + +(* + Atomic mutex lock taken from https://gitlab.com/gadmm/memprof-limits/-/blob/master/src/thread_map.ml#L23-34 +*) +val with_lock : Mutex.t -> scope:(unit -> 'a) -> 'a |