src/Pure/Thy/document_build.scala
changeset 77517 ede77a627b3a
parent 77510 f5d6cd98b16a
child 77520 84aa349ed597
--- a/src/Pure/Thy/document_build.scala	Sun Mar 05 15:19:53 2023 +0100
+++ b/src/Pure/Thy/document_build.scala	Sun Mar 05 15:25:02 2023 +0100
@@ -442,8 +442,9 @@
       directory: Directory,
       verbose: Boolean
     ): Document_Output = {
+      val progress = context.progress
       val result =
-        context.progress.bash(
+        progress.bash(
           build_script(context, directory),
           cwd = directory.doc_dir.file,
           echo = verbose,