--- a/etc/options Wed Jul 19 15:56:32 2023 +0200
+++ b/etc/options Wed Jul 19 16:04:59 2023 +0200
@@ -202,10 +202,10 @@
-- "slice size in MiB for ML heap stored within database"
option build_delay : real = 0.2
- -- "delay build process main loop"
+ -- "delay build process main loop (local)"
-option build_database_delay : real = 1.0
- -- "delay build process main loop (via central database)"
+option build_cluster_delay : real = 1.0
+ -- "delay build process main loop (cluster)"
section "Editor Session"
--- a/src/Pure/Tools/build_process.scala Wed Jul 19 15:56:32 2023 +0200
+++ b/src/Pure/Tools/build_process.scala Wed Jul 19 16:04:59 2023 +0200
@@ -879,8 +879,14 @@
}
catch { case exn: Throwable => close(); throw exn }
- protected val build_delay: Time =
- build_options.seconds(if (_build_database.isEmpty) "build_delay" else "build_database_delay")
+ protected val build_delay: Time = {
+ val option =
+ _build_database match {
+ case Some(db) if db.is_postgresql => "build_cluster_delay"
+ case _ => "build_delay"
+ }
+ build_options.seconds(option)
+ }
private val _host_database: Option[SQL.Database] =
try { store.maybe_open_build_database(path = Host.private_data.database, server = server) }