diff options
| author | Enrico Tassi | 2015-11-02 15:01:58 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2015-11-02 15:21:27 +0100 |
| commit | 6e376c8097d75b6e63a7e52332a721f7928992e9 (patch) | |
| tree | b62a39bd83f9770447141691ec0e395f2e80c5d0 | |
| parent | 559c0a4a40410745f73822e893b3d1581056ea7a (diff) | |
STM: fix undo into a branch containing side effects
The "master" label used to be reset to the wrong id
| -rw-r--r-- | stm/stm.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index a6a64f2094..89034706a4 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2333,7 +2333,9 @@ let edit_at id = let rec master_for_br root tip = if Stateid.equal tip Stateid.initial then tip else match VCS.visit tip with - | { step = (`Fork _ | `Sideff _ | `Qed _) } -> tip + | { step = (`Fork _ | `Qed _) } -> tip + | { step = `Sideff (`Ast(_,id)) } -> id + | { step = `Sideff _ } -> tip | { next } -> master_for_br root next in let reopen_branch start at_id mode qed_id tip old_branch = let master_id, cancel_switch, keep = |