etc/options
changeset 50505 33c92722cc3d
parent 50455 c7f366a861ed
child 50697 82e9178e6a98
     1.1 --- a/etc/options	Thu Dec 13 18:15:53 2012 +0100
     1.2 +++ b/etc/options	Thu Dec 13 19:53:55 2012 +0100
     1.3 @@ -96,5 +96,5 @@
     1.4  option editor_reparse_limit : int = 10000
     1.5    -- "maximum amount of reparsed text outside perspective"
     1.6  
     1.7 -option editor_tracing_limit_MB : real = 2.5
     1.8 -  -- "maximum tracing volume for each command transaction"
     1.9 +option editor_tracing_messages : int = 100
    1.10 +  -- "initial number of tracing messages for each command transaction"