etc/options
changeset 79928 cdc87eed26c7
parent 79915 40d2f9ce29fc
child 79948 8fe1ed4b5705
--- a/etc/options	Sun Mar 17 21:55:58 2024 +0100
+++ b/etc/options	Sun Mar 17 22:48:44 2024 +0100
@@ -222,6 +222,9 @@
 option build_schedule : string = ""
   -- "path to pre-computed schedule"
 
+option build_schedule_initial : string = ""
+  -- "path to initial pre-computed schedule (may be overwritten during build)"
+
 option build_schedule_outdated_delay : real = 300.0
   -- "delay schedule generation loop"