src/Tools/VSCode/src/vscode_rendering.scala
changeset 64759 100941134718
parent 64730 76996d915894
child 64762 cd545bec3fd0
     1.1 --- a/src/Tools/VSCode/src/vscode_rendering.scala	Mon Jan 02 18:08:04 2017 +0100
     1.2 +++ b/src/Tools/VSCode/src/vscode_rendering.scala	Tue Jan 03 14:17:03 2017 +0100
     1.3 @@ -126,7 +126,7 @@
     1.4        range, Nil, VSCode_Rendering.hyperlink_elements, _ =>
     1.5          {
     1.6            case (links, Text.Info(_, XML.Elem(Markup.Path(name), _))) =>
     1.7 -            val file = resources.append_file_url(snapshot.node_name.master_dir, name)
     1.8 +            val file = resources.append_file(snapshot.node_name.master_dir, name)
     1.9              Some(Line.Node_Range(file) :: links)
    1.10  
    1.11            case (links, Text.Info(info_range, XML.Elem(Markup(Markup.ENTITY, props), _))) =>