changeset 64664 | 951507563033 |
parent 63805 | c272680df665 |
child 65195 | ffab6f460a82 |
--- a/src/Pure/PIDE/query_operation.scala Fri Dec 23 15:53:53 2016 +0100 +++ b/src/Pure/PIDE/query_operation.scala Fri Dec 23 16:20:42 2016 +0100 @@ -208,7 +208,7 @@ for { command <- state.location snapshot = editor.node_snapshot(command.node_name) - link <- editor.hyperlink_command(true, snapshot, command) + link <- editor.hyperlink_command(true, snapshot, command.id) } link.follow(editor_context) }