tuned;
authorwenzelm
Tue Sep 11 19:43:06 2012 +0200 (2012-09-11)
changeset 4929064bed36cd8da
parent 49289 60424f123621
child 49291 66058a677ddd
tuned;
etc/options
     1.1 --- a/etc/options	Tue Sep 11 19:35:21 2012 +0200
     1.2 +++ b/etc/options	Tue Sep 11 19:43:06 2012 +0200
     1.3 @@ -81,7 +81,7 @@
     1.4    -- "timeout for session build job (seconds > 0)"
     1.5  
     1.6  
     1.7 -section {* Editor session parameters *}
     1.8 +section {* Editor reactivity *}
     1.9  
    1.10  option editor_load_delay : real = 0.5
    1.11    -- "delay for file load operations (new buffers etc.)"