diff options
Diffstat (limited to 'debugger/primitives.mli')
| -rw-r--r-- | debugger/primitives.mli | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/debugger/primitives.mli b/debugger/primitives.mli index 76526cf96f..8b03d8d2da 100644 --- a/debugger/primitives.mli +++ b/debugger/primitives.mli @@ -22,6 +22,10 @@ val nothing : 'a -> unit (*** Types and exceptions. ***) exception Out_of_range +(* [cleanup e f x] runs evaluates [f x] and reraises [e] with its original + backtrace. If [f x] raises, then [e] is not raised. *) +val cleanup : exn -> (unit -> unit) -> 'a + (*** Operations on lists. ***) (* Remove an element from a list *) |