# HG changeset patch
# User wenzelm
# Date 1606305465 -3600
# Node ID 1c42ac589fa0a303652cb33cfed9a82582f09714
# Parent  c6981f55e60d1eef2e48c96e2390634e987add9c
eliminated pointless transaction;

diff -r c6981f55e60d -r 1c42ac589fa0 src/Pure/Tools/build_job.scala
--- 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)