src/Pure/PIDE/command.scala
changeset 76858 39db5e268aaf
parent 76828 a5ff9cf61551
child 76879 cccd1a583c81
--- a/src/Pure/PIDE/command.scala	Sun Jan 01 22:01:53 2023 +0100
+++ b/src/Pure/PIDE/command.scala	Sun Jan 01 22:54:40 2023 +0100
@@ -464,7 +464,7 @@
           loaded_files.files.map(file =>
             (Exn.capture {
               val src_path = Path.explode(file)
-              val name = Document.Node.Name(resources.append(node_name.master_dir, src_path))
+              val name = Document.Node.Name(resources.append_path(node_name.master_dir, src_path))
               val content = get_blob(name).map(blob => (blob.bytes.sha1_digest, blob.chunk))
               Blob(name, src_path, content)
             }).user_error)