aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--stm/stm.ml4
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 =