equal
deleted
inserted
replaced
94 -- "delay for physical GUI updates" |
94 -- "delay for physical GUI updates" |
95 |
95 |
96 option editor_reparse_limit : int = 10000 |
96 option editor_reparse_limit : int = 10000 |
97 -- "maximum amount of reparsed text outside perspective" |
97 -- "maximum amount of reparsed text outside perspective" |
98 |
98 |
99 option editor_tracing_limit_MB : real = 2.5 |
99 option editor_tracing_messages : int = 100 |
100 -- "maximum tracing volume for each command transaction" |
100 -- "initial number of tracing messages for each command transaction" |