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)