diff -r 2cc6eab90cdf -r 33c92722cc3d etc/options --- a/etc/options Thu Dec 13 18:15:53 2012 +0100 +++ b/etc/options Thu Dec 13 19:53:55 2012 +0100 @@ -96,5 +96,5 @@ option editor_reparse_limit : int = 10000 -- "maximum amount of reparsed text outside perspective" -option editor_tracing_limit_MB : real = 2.5 - -- "maximum tracing volume for each command transaction" +option editor_tracing_messages : int = 100 + -- "initial number of tracing messages for each command transaction"