src/Pure/PIDE/command.scala
changeset 65488 331f09d9535e
parent 65359 9ca34f0407a9
child 65522 4d7c5df70a14
--- a/src/Pure/PIDE/command.scala	Mon Apr 17 12:11:02 2017 +0200
+++ b/src/Pure/PIDE/command.scala	Mon Apr 17 12:20:45 2017 +0200
@@ -451,8 +451,7 @@
         val blobs =
           files.map(file =>
             (Exn.capture {
-              val name =
-                Document.Node.Name(resources.append(node_name.master_dir, Path.explode(file)))
+              val name = Document.Node.Name(resources.append(node_name, Path.explode(file)))
               val blob = get_blob(name).map(blob => ((blob.bytes.sha1_digest, blob.chunk)))
               (name, blob)
             }).user_error)