src/Tools/jEdit/src/timing_dockable.scala
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)) }
   }