# HG changeset patch # User wenzelm # Date 1347385386 -7200 # Node ID 64bed36cd8da8d31761f8d9dea7da65314d50832 # Parent 60424f12362131c3d140fdb2bb0e9cf25898d9ad tuned; diff -r 60424f123621 -r 64bed36cd8da etc/options --- a/etc/options Tue Sep 11 19:35:21 2012 +0200 +++ b/etc/options Tue Sep 11 19:43:06 2012 +0200 @@ -81,7 +81,7 @@ -- "timeout for session build job (seconds > 0)" -section {* Editor session parameters *} +section {* Editor reactivity *} option editor_load_delay : real = 0.5 -- "delay for file load operations (new buffers etc.)"