src/Pure/Admin/build_doc.scala
changeset 75782 dba571dd0ba9
parent 75758 5ad049a5f6a8
child 76206 769a7cd5a16a
--- a/src/Pure/Admin/build_doc.scala	Sat Aug 06 17:28:59 2022 +0200
+++ b/src/Pure/Admin/build_doc.scala	Sat Aug 06 19:31:58 2022 +0200
@@ -54,9 +54,11 @@
             progress.expose_interrupt()
             progress.echo("Documentation " + quote(doc) + " ...")
 
-            using(store.open_database_context()) { db_context =>
-              Document_Build.build_documents(Document_Build.context(session, deps, db_context),
-                output_pdf = Some(Path.explode("~~/doc")))
+            using(Export.open_session_context(store, deps.base_info(session))) {
+              session_context =>
+                Document_Build.build_documents(
+                  Document_Build.context(session_context),
+                  output_pdf = Some(Path.explode("~~/doc")))
             }
             None
           }