diff -r 0e5339342998 -r dba571dd0ba9 src/Pure/Admin/build_doc.scala --- 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 }