diff options
| author | Emilio Jesus Gallego Arias | 2019-05-22 23:03:12 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-05-22 23:03:12 +0200 |
| commit | 20a464396fd89449569dc69b8cfb37cb69766733 (patch) | |
| tree | 0ee7ca0df404af94236829592765219c8213641a | |
| parent | 5c5bd952e9c28c3acf740fcdced03b2b7145076d (diff) | |
| parent | be9a1834a48393185ec9cfd9c18d157fd2a7ff02 (diff) | |
Merge PR #10173: Fail: don't catch critical errors
| -rw-r--r-- | vernac/vernacentries.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 918852239a..697bb788ac 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -2204,7 +2204,7 @@ let with_fail ~st f = try let _ = f () in raise HasNotFailed with | HasNotFailed as e -> raise e - | e -> + | e when CErrors.noncritical e || e = Timeout -> let e = CErrors.push e in raise (HasFailed (CErrors.iprint (ExplainErr.process_vernac_interp_error ~allow_uncaught:false e))) |