From 570744638ab4b08286562c0f4d45a7928ed008b0 Mon Sep 17 00:00:00 2001
From: Pierre Courtieu
Date: Fri, 22 Jan 2021 14:45:08 +0100
Subject: Fix #13739 - disable some warnings when calling Function.

Also added a generic way of temporarily disabling a warning.
Also added try_finalize un lib/utils.ml.
---
 lib/util.ml | 7 +++++++
 1 file changed, 7 insertions(+)

(limited to 'lib/util.ml')

diff --git a/lib/util.ml b/lib/util.ml
index 87cc30e557..e8aa0f3e48 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -135,6 +135,13 @@ type 'a delayed = unit -> 'a
 
 let delayed_force f = f ()
 
+(* finalize - Credit X.Leroy, D.Remy. *)
+let try_finally f x finally y =
+  let res = try f x with exn -> finally y; raise exn in
+  finally y;
+  res
+
+
 (* Misc *)
 
 type ('a, 'b) union = ('a, 'b) CSig.union = Inl of 'a | Inr of 'b
-- 
cgit v1.2.3