avoid hardwired parameters;
authorwenzelm
Fri, 02 Mar 2018 11:52:27 +0100
changeset 67743 7bd0a250183b
parent 67739 e512938b853c
child 67744 5c781dcd5864
avoid hardwired parameters; less ambitious defaults: low memory requirements;
etc/options
src/Pure/Admin/build_log.scala
--- 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))) }
       }