etc/options
changeset 79067 212c94edae2b
parent 78914 715f1bd21993
child 79289 7c1faa16554b
--- a/etc/options	Sun Nov 26 13:32:51 2023 +0100
+++ b/etc/options	Sun Nov 26 14:02:27 2023 +0100
@@ -273,10 +273,10 @@
 
 section "Headless Session"
 
-option headless_consolidate_delay : real = 15
+option headless_consolidate_delay : real = 2.0
   -- "delay to consolidate status of command evaluation (execution forks)"
 
-option headless_prune_delay : real = 60
+option headless_prune_delay : real = 30
   -- "delay to prune history (delete old versions)"
 
 option headless_check_delay : real = 0.5