diff options
| author | Enrico Tassi | 2014-09-08 13:46:44 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2014-09-09 13:11:38 +0200 |
| commit | b280ff870833a775564900d30d00a43d63246f8a (patch) | |
| tree | 0a877fc47af2e30f2f58945cda490efd9a685a93 /stm | |
| parent | 9d443eb0ff815a804f771335f0ac38a94d2851f2 (diff) | |
Undo: if the ui is coqtop (command line) then Undo is not part of the doc.
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/stm.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index f985cfe207..407c1ed1c7 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1466,7 +1466,8 @@ end = struct let id = VCS.get_branch_pos (VCS.current_branch ()) in let oid = fold_until (fun n (id,_,_) -> if Int.equal n 0 then `Stop id else `Cont (n-1)) n id in - VtStm (VtBack oid, true), VtLater + if n = 1 && !Flags.coqtop_ui then VtStm (VtBack oid, false), VtNow + else VtStm (VtBack oid, true), VtLater | VernacUndoTo _ | VernacRestart as e -> let m = match e with VernacUndoTo m -> m | _ -> 0 in |