changeset 72933 | fbc1d5ff3683 |
parent 72892 | d15c0c7ae092 |
child 73011 | 4519ba8da368 |
--- 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