--- 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))