src/Pure/Admin/build_doc.scala
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),