src/Pure/Thy/document_build.scala
changeset 77521 5642de4d225d
parent 77520 84aa349ed597
child 77541 9d9b30741fc4
--- a/src/Pure/Thy/document_build.scala	Sun Mar 05 16:26:59 2023 +0100
+++ b/src/Pure/Thy/document_build.scala	Sun Mar 05 16:36:18 2023 +0100
@@ -586,7 +586,7 @@
         progress.interrupt_handler {
           val build_results =
             Build.build(options, selection = Sessions.Selection.session(session),
-              dirs = dirs, progress = progress, verbose = progress.verbose)
+              dirs = dirs, progress = progress)
           if (!build_results.ok) error("Failed to build session " + quote(session))
 
           if (output_sources.isEmpty && output_pdf.isEmpty) {