# HG changeset patch
# User wenzelm
# Date 1519987947 -3600
# Node ID 7bd0a250183bf5ebe129d5db659bf91921efa710
# Parent  e512938b853cfe2411bcf7876ada4374b0552ca6
avoid hardwired parameters;
less ambitious defaults: low memory requirements;

diff -r e512938b853c -r 7bd0a250183b etc/options
--- 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"
diff -r e512938b853c -r 7bd0a250183b src/Pure/Admin/build_log.scala
--- 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))) }
       }