author | wenzelm |
Wed, 25 Nov 2020 12:57:45 +0100 | |
changeset 72701 | 1c42ac589fa0 |
parent 72700 | c6981f55e60d |
child 72702 | 79a19657c170 |
--- a/src/Pure/Tools/build_job.scala Wed Nov 25 12:55:09 2020 +0100 +++ b/src/Pure/Tools/build_job.scala Wed Nov 25 12:57:45 2020 +0100 @@ -239,11 +239,7 @@ progress = progress, verbose = verbose)) using(store.open_database(session_name, output = true))(db => - for (doc <- documents) { - db.transaction { - doc.write(db, session_name) - } - }) + documents.foreach(_.write(db, session_name))) (documents.flatMap(_.log_lines), Nil) } (Nil, Nil)