changeset 76656 | a8f452f7c503 |
parent 76455 | 74c3ecfeb3ea |
child 76741 | ec07b1af45c5 |
--- a/src/Pure/Admin/build_doc.scala Fri Dec 16 17:30:29 2022 +0100 +++ b/src/Pure/Admin/build_doc.scala Fri Dec 16 17:51:52 2022 +0100 @@ -54,7 +54,7 @@ progress.expose_interrupt() progress.echo("Documentation " + quote(doc) + " ...") - using(Export.open_session_context(build_results.store, deps.base_info(session))) { + using(Export.open_session_context(build_results.store, deps.background(session))) { session_context => Document_Build.build_documents( Document_Build.context(session_context),