--- a/etc/options Thu Mar 01 20:44:38 2018 +0100
+++ b/etc/options Fri Mar 02 11:52:27 2018 +0100
@@ -256,3 +256,4 @@
option build_log_ssh_user : string = ""
option build_log_ssh_port : int = 0
option build_log_history : int = 30 -- "length of relevant history (in days)"
+option build_log_transaction_size : int = 1 -- "number of log files for each db update"
--- 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))) }
}