etc/options
changeset 69103 814a1ab42d70
parent 68661 5820f0f379ae
child 69353 a6e83dcc00e6
     1.1 --- a/etc/options	Mon Oct 01 19:30:36 2018 +0200
     1.2 +++ b/etc/options	Tue Oct 02 19:02:47 2018 +0200
     1.3 @@ -174,7 +174,7 @@
     1.4    -- "maximum amount of reparsed text outside perspective"
     1.5  
     1.6  public option editor_tracing_messages : int = 1000
     1.7 -  -- "initial number of tracing messages for each command transaction"
     1.8 +  -- "initial number of tracing messages for each command transaction (0: unbounded)"
     1.9  
    1.10  public option editor_chart_delay : real = 3.0
    1.11    -- "delay for chart repainting"