clarified options;
authorwenzelm
Wed, 19 Jul 2023 16:04:59 +0200
changeset 78409 f2d67c78b689
parent 78408 092f1e435b3a
child 78410 c5170293d392
clarified options;
etc/options
src/Pure/Tools/build_process.scala
--- 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) }