# HG changeset patch
# User wenzelm
# Date 1636920894 -3600
# Node ID f118008a81314e9c392b8f0f59bb2624251477e3
# Parent  543f932f64b8d56e75ae427cbd1a4562e24574e2
tuned signature (again): latex_output is likely to depend on context;

diff -r 543f932f64b8 -r f118008a8131 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 =