# HG changeset patch
# User wenzelm
# Date 1671628442 -3600
# Node ID 872fc664cd9975808f715965e4a036e4bb45abc6
# Parent  1b8dd8c0492fd77aeb9c33d1282ec3f58a936aef
tuned signature;

diff -r 1b8dd8c0492f -r 872fc664cd99 src/Pure/Thy/document_build.scala
--- a/src/Pure/Thy/document_build.scala	Wed Dec 21 14:00:00 2022 +0100
+++ b/src/Pure/Thy/document_build.scala	Wed Dec 21 14:14:02 2022 +0100
@@ -141,7 +141,7 @@
   final class Context private[Document_Build](
     val session_context: Export.Session_Context,
     document_session: Option[Sessions.Base],
-    val progress: Progress = new Progress
+    val progress: Progress
   ) {
     context =>
 
@@ -526,8 +526,8 @@
             progress.echo_warning("No output directory")
           }
 
-          val background = session_background(options, session, dirs = dirs)
-          using(Export.open_session_context(build_results.store, background)) {
+          val session_background = Document_Build.session_background(options, session, dirs = dirs)
+          using(Export.open_session_context(build_results.store, session_background)) {
             session_context =>
               build_documents(
                 context(session_context, progress = progress),