diff options
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/stm.ml | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index ad94b6807..dbecbdae5 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2803,6 +2803,11 @@ let process_transaction ?(newtip=Stateid.fresh ()) ?(part_of_script=true) (* Meta *) | VtMeta, _ -> let id, w = Backtrack.undo_vernac_classifier expr in + (* Special case Backtrack, as it is never part of a script. See #6240 *) + let part_of_script = begin match Vernacprop.under_control expr with + | VernacBacktrack _ -> false + | _ -> part_of_script + end in process_back_meta_command ~part_of_script ~newtip ~head id x w (* Query *) | VtQuery (false,route), VtNow -> |