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"