etc/options
changeset 49290 64bed36cd8da
parent 49288 2c9272cb4568
child 49295 2750756db9c5
     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.)"