# HG changeset patch
# User wenzelm
# Date 1671557631 -3600
# Node ID 4db6852313269edf7d463beafe8704b1fe16c345
# Parent  a7602257a8257340c3dbe79561f743136648a256
tuned signature;

diff -r a7602257a825 -r 4db685231326 src/Pure/Thy/document_build.scala
--- a/src/Pure/Thy/document_build.scala	Tue Dec 20 16:34:13 2022 +0100
+++ b/src/Pure/Thy/document_build.scala	Tue Dec 20 18:33:51 2022 +0100
@@ -115,10 +115,11 @@
     options: Options,
     session: String,
     dirs: List[Path] = Nil,
-    progress: Progress = new Progress
+    progress: Progress = new Progress,
+    verbose: Boolean = false
   ): Sessions.Background = {
       Sessions.load_structure(options + "document=pdf", dirs = dirs).
-        selection_deps(Sessions.Selection.session(session), progress = progress).
+        selection_deps(Sessions.Selection.session(session), progress = progress, verbose = verbose).
         background(session)
   }