# HG changeset patch
# User wenzelm
# Date 1689680058 -7200
# Node ID c39819e3adc5c2db7201f22f04053752365f2570
# Parent  761d12b043d00da0ef448c0448c49ef34e024795
more conservative build_delay (despite 9600720071e6): avoid exessive build_database operations, notably via ssh;

diff -r 761d12b043d0 -r c39819e3adc5 etc/options
--- a/etc/options	Tue Jul 18 13:32:34 2023 +0200
+++ b/etc/options	Tue Jul 18 13:34:18 2023 +0200
@@ -198,7 +198,7 @@
 option build_database_slice : real = 300
   -- "slice size in MiB for ML heap stored within database"
 
-option build_delay : real = 0.2
+option build_delay : real = 0.5
   -- "delay build process main loop"