diff options
| author | Enrico Tassi | 2019-01-10 15:02:03 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2019-01-10 15:07:14 +0100 |
| commit | c01017cbde71a9af0707594d33d1af2b6b5b2186 (patch) | |
| tree | 34b0d8a3e847a64707591d207c213cc8c435cfe0 | |
| parent | 2438fe12017323c32a57e0c56120c3c0f339ec6b (diff) | |
[STM] kill no_safe_id anomaly
| -rw-r--r-- | stm/stm.ml | 14 |
1 files changed, 3 insertions, 11 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index 036b8d7969..169d608d2d 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2831,17 +2831,9 @@ let merge_proof_branch ~valid ?id qast keep brname = (* When tty is true, this code also does some of the job of the user interface: jump back to a state that is valid *) let handle_failure (e, info) vcs = - match Stateid.get info with - | None -> - VCS.restore vcs; - VCS.print (); - anomaly(str"error with no safe_id attached:" ++ spc() ++ - CErrors.iprint_no_report (e, info) ++ str".") - | Some (safe_id, id) -> - stm_prerr_endline (fun () -> "Failed at state " ^ Stateid.to_string id); - VCS.restore vcs; - VCS.print (); - Exninfo.iraise (e, info) + VCS.restore vcs; + VCS.print (); + Exninfo.iraise (e, info) let snapshot_vio ~doc ldir long_f_dot_vo = let doc = finish ~doc in |