etc/options
changeset 79289 7c1faa16554b
parent 79067 212c94edae2b
child 79483 299568e54fac
--- a/etc/options	Thu Dec 14 13:03:33 2023 +0100
+++ b/etc/options	Thu Dec 14 13:10:01 2023 +0100
@@ -213,6 +213,12 @@
 option build_cluster_identifier : string = "build_cluster"
   -- "ISABELLE_IDENTIFIER for remote build cluster sessions"
 
+option build_schedule_outdated_delay : real = 300.0
+  -- "delay schedule generation loop"
+
+option build_schedule_outdated_limit : int = 20
+  -- "maximum number of sessions for which schedule stays valid"
+
 
 section "Editor Session"