diff options
| author | Gaëtan Gilbert | 2019-05-16 13:15:12 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-05-17 14:33:28 +0200 |
| commit | be9a1834a48393185ec9cfd9c18d157fd2a7ff02 (patch) | |
| tree | 5f550b3a8655adeaa9686932bb12a850c3c13ce4 | |
| parent | e9c2bc9aaddd401d18d90411ff68644b1d05c0d5 (diff) | |
Fail: don't catch critical errors
Not sure why we didn't. Fail didn't catch anomalies almost by accident.
It still makes sense to catch Timeout here imo
| -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 e1d134f3a9..7bb4f71014 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))) |