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)