changeset 76826 | eb3b946bdeff |
parent 76769 | 0438622a7b9c |
child 76884 | a004c5322ea4 |
--- a/src/Pure/Thy/document_build.scala Fri Dec 30 12:41:08 2022 +0100 +++ b/src/Pure/Thy/document_build.scala Fri Dec 30 13:25:29 2022 +0100 @@ -140,7 +140,7 @@ def content: File.Content_XML = File.content(Path.basic(tex_name(name)), body) def file_pos: String = name.path.implode_symbolic def write(latex_output: Latex.Output, dir: Path): Unit = - content.output(latex_output(_, file_pos = file_pos)).write(dir) + content.output(latex_output.make(_, file_pos = file_pos)).write(dir) } def context(