src/Tools/jEdit/src/jedit_rendering.scala
changeset 65488 331f09d9535e
parent 65487 7847807b07ce
child 65911 f97d163479b9
--- a/src/Tools/jEdit/src/jedit_rendering.scala	Mon Apr 17 12:11:02 2017 +0200
+++ b/src/Tools/jEdit/src/jedit_rendering.scala	Mon Apr 17 12:20:45 2017 +0200
@@ -304,7 +304,7 @@
       range, Vector.empty, JEdit_Rendering.hyperlink_elements, _ =>
         {
           case (links, Text.Info(info_range, XML.Elem(Markup.Path(name), _))) =>
-            val file = perhaps_append_file(snapshot.node_name.master_dir, name)
+            val file = perhaps_append_file(snapshot.node_name, name)
             val link = JEdit_Editor.hyperlink_file(true, file)
             Some(links :+ Text.Info(snapshot.convert(info_range), link))