src/Pure/Tools/build_job.scala
changeset 75970 b4a04fa01677
parent 75914 4da80799352f
child 76087 c8f5fec36b5c
--- a/src/Pure/Tools/build_job.scala	Thu Aug 25 15:58:17 2022 +0200
+++ b/src/Pure/Tools/build_job.scala	Thu Aug 25 16:05:33 2022 +0200
@@ -456,7 +456,7 @@
                       output_sources = info.document_output,
                       output_pdf = info.document_output)
                 }
-              using(database_context.open_output_database(session_name))(session_database =>
+              using(database_context.open_database(session_name, output = true))(session_database =>
                 documents.foreach(_.write(session_database.db, session_name)))
               (documents.flatMap(_.log_lines), Nil)
             }