From be9a1834a48393185ec9cfd9c18d157fd2a7ff02 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 16 May 2019 13:15:12 +0200
Subject: 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
---
 vernac/vernacentries.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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)))
-- 
cgit v1.2.3