diff options
| author | Pierre-Marie Pédrot | 2020-11-23 11:19:49 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-11-23 11:19:49 +0100 |
| commit | 8b3ad4dc37b55fbf2420b692c352a1c748181411 (patch) | |
| tree | c60d947fcb47c8513e05d2255020b85b12f3a28d /lib/cErrors.ml | |
| parent | 0326d06211c49efb4018d65280cf26340f7344b4 (diff) | |
| parent | 6eb6f55499647b9b5a72626839683f6dff9c1549 (diff) | |
Merge PR #13377: Fix timeout by ensuring signal exceptions are not erroneously caught
Reviewed-by: ppedrot
Diffstat (limited to 'lib/cErrors.ml')
| -rw-r--r-- | lib/cErrors.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/lib/cErrors.ml b/lib/cErrors.ml index cb64e36755..760c07783b 100644 --- a/lib/cErrors.ml +++ b/lib/cErrors.ml @@ -37,7 +37,7 @@ let user_err ?loc ?info ?hdr strm = let info = Option.cata (Loc.add_loc info) info loc in Exninfo.iraise (UserError (hdr, strm), info) -exception Timeout +exception Timeout = Control.Timeout (** Only anomalies should reach the bottom of the handler stack. In usual situation, the [handle_stack] is treated as it if was always @@ -135,7 +135,7 @@ let _ = register_handler begin function | UserError(s, pps) -> Some (where s ++ pps) | _ -> None -end + end (** Critical exceptions should not be caught and ignored by mistake by inner functions during a [vernacinterp]. They should be handled @@ -145,7 +145,7 @@ end let noncritical = function | Sys.Break | Out_of_memory | Stack_overflow | Assert_failure _ | Match_failure _ | Anomaly _ - | Timeout -> false + | Control.Timeout -> false | Invalid_argument "equal: functional value" -> false | _ -> true [@@@ocaml.warning "+52"] |