etc/options
changeset 50455 c7f366a861ed
parent 50255 d0ec1f0d1d7d
child 50505 33c92722cc3d
     1.1 --- a/etc/options	Mon Dec 10 15:46:50 2012 +0100
     1.2 +++ b/etc/options	Mon Dec 10 16:06:57 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 : int = 1000000
     1.8 +option editor_tracing_limit_MB : real = 2.5
     1.9    -- "maximum tracing volume for each command transaction"