aboutsummaryrefslogtreecommitdiff
path: root/plugins/ssr
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2020-03-04 11:25:51 +0100
committerPierre-Marie Pédrot2020-03-04 11:25:51 +0100
commit89f111f2e15d8cab61495a419f0c9f7ae95e086a (patch)
tree300ebf99c79fe0e91faf2ad50439b17916e60cf7 /plugins/ssr
parent2937fe5c1bb14a7cb7f00bb6e8d418ece00a7f50 (diff)
parentb2c58a23a1f71c86d8a64147923214b5059bd747 (diff)
Merge PR #11380: [exninfo] Deprecate aliases for exception re-raising.
Reviewed-by: Matafou Reviewed-by: ppedrot
Diffstat (limited to 'plugins/ssr')
-rw-r--r--plugins/ssr/ssrcommon.ml8
1 files changed, 4 insertions, 4 deletions
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index f95672a15d..6ff79ebb9b 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -1095,11 +1095,11 @@ let tclDO n tac =
try tac gl
with
| CErrors.UserError (l, s) as e ->
- let _, info = CErrors.push e in
- let e' = CErrors.UserError (l, prefix i ++ s) in
- Util.iraise (e', info)
+ let _, info = Exninfo.capture e in
+ let e' = CErrors.UserError (l, prefix i ++ s) in
+ Exninfo.iraise (e', info)
| Gramlib.Ploc.Exc(loc, CErrors.UserError (l, s)) ->
- raise (Gramlib.Ploc.Exc(loc, CErrors.UserError (l, prefix i ++ s))) in
+ raise (Gramlib.Ploc.Exc(loc, CErrors.UserError (l, prefix i ++ s))) in
let rec loop i gl =
if i = n then tac_err_at i gl else
(tclTHEN (tac_err_at i) (loop (i + 1))) gl in