changeset 76739 | cb72b5996520 |
parent 76666 | 981801179bc5 |
child 76766 | 235de80d4b25 |
--- a/src/Pure/PIDE/resources.scala Thu Dec 22 08:56:16 2022 +0100 +++ b/src/Pure/PIDE/resources.scala Thu Dec 22 15:23:26 2022 +0100 @@ -70,6 +70,8 @@ /* file-system operations */ + def migrate_name(name: Document.Node.Name): Document.Node.Name = name + def append(dir: String, source_path: Path): String = (Path.explode(dir) + source_path).expand.implode