etc/options
changeset 49290 64bed36cd8da
parent 49288 2c9272cb4568
child 49295 2750756db9c5
equal deleted inserted replaced
49289:60424f123621 49290:64bed36cd8da
    79 
    79 
    80 option timeout : real = 0
    80 option timeout : real = 0
    81   -- "timeout for session build job (seconds > 0)"
    81   -- "timeout for session build job (seconds > 0)"
    82 
    82 
    83 
    83 
    84 section {* Editor session parameters *}
    84 section {* Editor reactivity *}
    85 
    85 
    86 option editor_load_delay : real = 0.5
    86 option editor_load_delay : real = 0.5
    87   -- "delay for file load operations (new buffers etc.)"
    87   -- "delay for file load operations (new buffers etc.)"
    88 
    88 
    89 option editor_input_delay : real = 0.3
    89 option editor_input_delay : real = 0.3