--- a/src/Pure/Tools/build_job.scala Mon Jul 17 12:22:39 2023 +0200
+++ b/src/Pure/Tools/build_job.scala Mon Jul 17 15:31:42 2023 +0200
@@ -389,7 +389,7 @@
val (document_output, document_errors) =
try {
if (build_errors.isInstanceOf[Exn.Res[_]] && result0.ok && info.documents.nonEmpty) {
- using(Export.open_database_context(store)) { database_context =>
+ using(Export.open_database_context(store, server = server)) { database_context =>
val documents =
using(database_context.open_session(session_background)) {
session_context =>