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,