changeset 60893 | 3c8b9b4b577c |
parent 60890 | e2aeaa397e93 |
child 60897 | 7aad4be8a48e |
--- a/src/Tools/jEdit/src/debugger_dockable.scala Tue Aug 11 15:24:49 2015 +0200 +++ b/src/Tools/jEdit/src/debugger_dockable.scala Tue Aug 11 17:00:16 2015 +0200 @@ -321,7 +321,7 @@ private def update_focus(focus: Option[Position.T]) { if (Debugger.focus(focus) && focus.isDefined) - PIDE.editor.hyperlink_position(current_snapshot, focus.get).foreach(_.follow(view)) + PIDE.editor.hyperlink_position(false, current_snapshot, focus.get).foreach(_.follow(view)) }