etc/options
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"