# HG changeset patch
# User wenzelm
# Date 1689775499 -7200
# Node ID f2d67c78b6897af0f9e6436004da05cb569a3e09
# Parent  092f1e435b3a6f8a23453b7dbed97faa84281d9c
clarified options;

diff -r 092f1e435b3a -r f2d67c78b689 etc/options
--- 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"
diff -r 092f1e435b3a -r f2d67c78b689 src/Pure/Tools/build_process.scala
--- 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) }