src/Pure/Tools/build_job.scala
changeset 72700 c6981f55e60d
parent 72699 ed59a506998f
child 72701 1c42ac589fa0
--- a/src/Pure/Tools/build_job.scala	Wed Nov 25 12:52:00 2020 +0100
+++ b/src/Pure/Tools/build_job.scala	Wed Nov 25 12:55:09 2020 +0100
@@ -241,7 +241,7 @@
             using(store.open_database(session_name, output = true))(db =>
               for (doc <- documents) {
                 db.transaction {
-                  Presentation.write_document(db, session_name, doc)
+                  doc.write(db, session_name)
                 }
               })
             (documents.flatMap(_.log_lines), Nil)