src/Pure/Thy/document_build.scala
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(