--- a/src/Tools/jEdit/src/jedit_editor.scala Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Tools/jEdit/src/jedit_editor.scala Fri Mar 27 22:01:27 2020 +0100
@@ -202,7 +202,7 @@
case doc: Doc.Text_File if doc.name == name => doc.path
case doc: Doc.Doc if doc.name == name => doc.path}).map(path =>
new Hyperlink {
- override val external = !path.is_file
+ override val external: Boolean = !path.is_file
def follow(view: View): Unit = goto_doc(view, path)
override def toString: String = "doc " + quote(name)
})