equal
deleted
inserted
replaced
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 |