changeset 64663 | 4c9fb4d4bca3 |
parent 64524 | e6a3c55b929b |
child 64664 | 951507563033 |
--- a/src/Pure/PIDE/editor.scala Fri Dec 23 11:53:31 2016 +0100 +++ b/src/Pure/PIDE/editor.scala Fri Dec 23 15:53:53 2016 +0100 @@ -24,7 +24,7 @@ def remove_overlay(command: Command, fn: String, args: List[String]): Unit abstract class Hyperlink { - def external: Boolean + def external: Boolean = false def follow(context: Context): Unit } def hyperlink_command(