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