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