# HG changeset patch
# User wenzelm
# Date 1608129857 -3600
# Node ID fbc1d5ff3683429bbe76899b8ef01a3227d29f2d
# Parent  f7954a960890e5d5462bc787f1c02a21496233c0
afford more reactive input;

diff -r f7954a960890 -r fbc1d5ff3683 etc/options
--- a/etc/options	Wed Dec 16 15:39:21 2020 +0100
+++ b/etc/options	Wed Dec 16 15:44:17 2020 +0100
@@ -159,7 +159,7 @@
 public option editor_load_delay : real = 0.5
   -- "delay for file load operations (new buffers etc.)"
 
-public option editor_input_delay : real = 0.3
+public option editor_input_delay : real = 0.2
   -- "delay for user input (text edits, cursor movement etc.)"
 
 public option editor_generated_input_delay : real = 1.0