diff options
Diffstat (limited to 'lib/future.ml')
| -rw-r--r-- | lib/future.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/lib/future.ml b/lib/future.ml index 5cccd2038d..ddf841b7fc 100644 --- a/lib/future.ml +++ b/lib/future.ml @@ -28,9 +28,9 @@ exception NotReady of string exception NotHere of string let _ = CErrors.register_handler (function - | NotReady name -> !not_ready_msg name - | NotHere name -> !not_here_msg name - | _ -> raise CErrors.Unhandled) + | NotReady name -> Some (!not_ready_msg name) + | NotHere name -> Some (!not_here_msg name) + | _ -> None) type fix_exn = Exninfo.iexn -> Exninfo.iexn let id x = x |