diff options
| -rw-r--r-- | ide/coqOps.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/ide/coqOps.ml b/ide/coqOps.ml index ab70e35b98..be9075279b 100644 --- a/ide/coqOps.ml +++ b/ide/coqOps.ml @@ -625,7 +625,8 @@ object(self) if loc <> None then messages#push Error "Fixme LOC"; messages#push Error msg; if Stateid.equal safe_id Stateid.dummy then self#show_goals - else undo safe_id (Doc.is_in_focus document safe_id)) + else undo safe_id + (Doc.focused document && Doc.is_in_focus document safe_id)) in undo to_id unfocus_needed) |