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"