etc/options
changeset 79883 6fa259b24deb
parent 79814 2da08d9ce629
child 79886 7ae25372ab04
--- a/etc/options	Wed Mar 13 11:04:06 2024 +0100
+++ b/etc/options	Wed Mar 13 11:23:22 2024 +0100
@@ -207,6 +207,9 @@
 option build_cluster_delay : real = 1.0
   -- "delay build process main loop (cluster)"
 
+option build_cluster_expire : int = 50
+  -- "enforce database synchronization after given number of delay loops"
+
 option build_cluster_root : string = "$USER_HOME/.isabelle/build_cluster"
   -- "root directory for remote build cluster sessions"