equal
deleted
inserted
replaced
95 -- "timeout for session build job (seconds > 0)" |
95 -- "timeout for session build job (seconds > 0)" |
96 |
96 |
97 option process_output_limit : int = 100 |
97 option process_output_limit : int = 100 |
98 -- "build process output limit in million characters (0 = unlimited)" |
98 -- "build process output limit in million characters (0 = unlimited)" |
99 |
99 |
|
100 public option exception_trace : bool = false |
|
101 -- "exception trace for toplevel command execution" |
|
102 |
100 |
103 |
101 section "Editor Reactivity" |
104 section "Editor Reactivity" |
102 |
105 |
103 public option editor_load_delay : real = 0.5 |
106 public option editor_load_delay : real = 0.5 |
104 -- "delay for file load operations (new buffers etc.)" |
107 -- "delay for file load operations (new buffers etc.)" |