diff options
| author | Enrico Tassi | 2016-09-06 15:07:43 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2016-09-06 15:07:43 +0200 |
| commit | 83ec679e785f5313f088be77bcd652a29783623b (patch) | |
| tree | 4358e8b0ae3ce09436539a7a2439161dbf40e2c6 | |
| parent | ea71f4d2abefd0c26c247268250aa9396f717ea8 (diff) | |
STM: queries give back a dummy safe_id in case of error (#5041)
| -rw-r--r-- | stm/stm.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index e5902c0535..ac24bfc492 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2471,12 +2471,12 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty {x with verbose = true } with e when CErrors.noncritical e -> let e = CErrors.push e in - iraise (State.exn_on report_id e)); `Ok + iraise (State.exn_on ~valid:Stateid.dummy report_id e)); `Ok | VtQuery (false,(report_id,route)), VtNow -> (try vernac_interp report_id ~route x with e -> let e = CErrors.push e in - iraise (State.exn_on report_id e)); `Ok + iraise (State.exn_on ~valid:Stateid.dummy report_id e)); `Ok | VtQuery (true,(report_id,_)), w -> assert(Stateid.equal report_id Stateid.dummy); let id = VCS.new_node ~id:newtip () in |