summaryrefslogtreecommitdiff
path: root/stdlib/stdlib.mli
diff options
context:
space:
mode:
authorTom Kelly <ctk21@cl.cam.ac.uk>2020-04-17 09:50:14 +0100
committerTom Kelly <ctk21@cl.cam.ac.uk>2020-04-17 09:50:14 +0100
commitc28d770ba4686b2bad202106896a0eb4eccc1ff2 (patch)
treee3e7e250997a224b74379eff5f34da1e59af7a99 /stdlib/stdlib.mli
parent3d761df20b2e3a56b834622cf6926d64085c15f6 (diff)
parent6fb33f712bdca2da7ee1dd18f49402c3203f8e1e (diff)
downloadocaml-c28d770ba4686b2bad202106896a0eb4eccc1ff2.tar.gz
Merge commit '6fb33f712bdca2da7ee1dd18f49402c3203f8e1e' into parallel_minor_gc_4_09
Diffstat (limited to 'stdlib/stdlib.mli')
-rw-r--r--stdlib/stdlib.mli9
1 files changed, 0 insertions, 9 deletions
diff --git a/stdlib/stdlib.mli b/stdlib/stdlib.mli
index 2a3937df16..f8f512da59 100644
--- a/stdlib/stdlib.mli
+++ b/stdlib/stdlib.mli
@@ -44,15 +44,6 @@ exception Exit
(** The [Exit] exception is not raised by any library function. It is
provided for use in your programs. *)
-val protect : finally:(unit -> unit) -> (unit -> 'a) -> 'a
-(** [protect ~finally work] invokes [work ()] and then [finally ()]
- before [work] returns with its value or an exception. In the latter
- case the exception is re-raised after [finally ()].
- If [finally ()] raises, this exception is not caught and may shadow
- one [work ()] may have raised.
-
- @since 4.08.0 *)
-
(** {6 Effects} *)
(** [perform e] performs an effect [e].