tuned signature (again): latex_output is likely to depend on context;
authorwenzelm
Sun, 14 Nov 2021 21:14:54 +0100
changeset 74787 f118008a8131
parent 74786 543f932f64b8
child 74788 95e514137861
tuned signature (again): latex_output is likely to depend on context;
src/Pure/Thy/document_build.scala
--- a/src/Pure/Thy/document_build.scala	Sun Nov 14 20:40:41 2021 +0100
+++ b/src/Pure/Thy/document_build.scala	Sun Nov 14 21:14:54 2021 +0100
@@ -359,9 +359,8 @@
 
   abstract class Bash_Engine(name: String) extends Engine(name)
   {
-    def latex_output: Latex.Output = new Latex.Output
     def prepare_directory(context: Context, dir: Path, doc: Document_Variant): Directory =
-      context.prepare_directory(dir, doc, latex_output)
+      context.prepare_directory(dir, doc, new Latex.Output)
 
     def use_pdflatex: Boolean = false
     def latex_script(context: Context, directory: Directory): String =