diff options
| author | Pierre-Marie Pédrot | 2015-07-18 12:18:05 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-07-18 12:18:05 +0200 |
| commit | 88e2da8c1b9403f5eac19df4f6c55fedca948bcc (patch) | |
| tree | 01f750142359361f800e0dc2dfe422f145f491c5 /stm | |
| parent | 139c92bebd3f3d22c9f4d8220647bb7dd4e43890 (diff) | |
| parent | fdd6a17b272995237c9f95fc465bb1ff6871bedc (diff) | |
Merge branch 'v8.5'
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/stm.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index 373fd0ba39..8af1aaafdc 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2117,7 +2117,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) = iraise (State.exn_on report_id e)); `Ok | VtQuery (false,(report_id,route)), VtNow -> (try vernac_interp report_id ~route x - with e when Errors.noncritical e -> + with e -> let e = Errors.push e in iraise (State.exn_on report_id e)); `Ok | VtQuery (true,(report_id,_)), w -> |