etc/options
changeset 78395 c39819e3adc5
parent 78364 e33cca11b474
child 78400 63d55ba90a9f
equal deleted inserted replaced
78394:761d12b043d0 78395:c39819e3adc5
   196   -- "expose state of build process via central database"
   196   -- "expose state of build process via central database"
   197 
   197 
   198 option build_database_slice : real = 300
   198 option build_database_slice : real = 300
   199   -- "slice size in MiB for ML heap stored within database"
   199   -- "slice size in MiB for ML heap stored within database"
   200 
   200 
   201 option build_delay : real = 0.2
   201 option build_delay : real = 0.5
   202   -- "delay build process main loop"
   202   -- "delay build process main loop"
   203 
   203 
   204 
   204 
   205 section "Editor Session"
   205 section "Editor Session"
   206 
   206