changeset 78364 | e33cca11b474 |
parent 78309 | fc6246225283 |
child 78395 | c39819e3adc5 |
--- a/etc/options Sun Jul 16 13:45:46 2023 +0200 +++ b/etc/options Sun Jul 16 14:11:56 2023 +0200 @@ -198,6 +198,9 @@ option build_database_slice : real = 300 -- "slice size in MiB for ML heap stored within database" +option build_delay : real = 0.2 + -- "delay build process main loop" + section "Editor Session"