diff options
| author | Pierre Courtieu | 2021-01-22 14:45:08 +0100 |
|---|---|---|
| committer | Pierre Courtieu | 2021-02-03 17:15:01 +0100 |
| commit | 570744638ab4b08286562c0f4d45a7928ed008b0 (patch) | |
| tree | 75bba9ef80c938a90afb653410aace2974054b2c /lib/util.ml | |
| parent | 8615aac5fc342b2184b3431abec15dbab621efba (diff) | |
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.
Diffstat (limited to 'lib/util.ml')
| -rw-r--r-- | lib/util.ml | 7 |
1 files changed, 7 insertions, 0 deletions
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 |