--- a/src/Pure/Admin/build_log.scala Thu Mar 01 20:44:38 2018 +0100
+++ b/src/Pure/Admin/build_log.scala Fri Mar 02 11:52:27 2018 +0100
@@ -1101,7 +1101,10 @@
}
})
- for (file_group <- files.filter(file => status.exists(_.required(file))).grouped(100)) {
+ for (file_group <-
+ files.filter(file => status.exists(_.required(file))).
+ grouped(options.int("build_log_transaction_size") max 1))
+ {
val log_files = Par_List.map[JFile, Log_File](Log_File.apply _, file_group)
db.transaction { log_files.foreach(log_file => status.foreach(_.update(log_file))) }
}