author | wenzelm |
Tue, 07 Aug 2012 17:46:30 +0200 | |
changeset 48711 | 8d381fdef898 |
parent 48710 | 5b51ccdc8623 |
child 48712 | 6b7a9bcc0bae |
--- a/src/Pure/Thy/thy_load.scala Tue Aug 07 17:08:22 2012 +0200 +++ b/src/Pure/Thy/thy_load.scala Tue Aug 07 17:46:30 2012 +0200 @@ -39,7 +39,7 @@ /* file-system operations */ def append(dir: String, source_path: Path): String = - (Path.explode(dir) + source_path).implode + (Path.explode(dir) + source_path).expand.implode def read_header(name: Document.Node.Name): Thy_Header = {