| author | wenzelm | 
| Tue, 18 Jul 2023 13:34:18 +0200 | |
| changeset 78395 | c39819e3adc5 | 
| parent 78394 | 761d12b043d0 | 
| child 78396 | 7853d9072d1b | 
| etc/options | file | annotate | diff | comparison | revisions | 
--- 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"