changeset 64664 | 951507563033 |
parent 64443 | 857acb970dfa |
child 64854 | f5aa712e6250 |
--- a/src/Tools/jEdit/src/timing_dockable.scala Fri Dec 23 15:53:53 2016 +0100 +++ b/src/Tools/jEdit/src/timing_dockable.scala Fri Dec 23 16:20:42 2016 +0100 @@ -96,7 +96,7 @@ def print: String = " " + Time.print_seconds(timing) + "s command " + quote(command.span.name) def follow(snapshot: Document.Snapshot) - { PIDE.editor.hyperlink_command(true, snapshot, command).foreach(_.follow(view)) } + { PIDE.editor.hyperlink_command(true, snapshot, command.id).foreach(_.follow(view)) } }