etc/options
changeset 50697 82e9178e6a98
parent 50505 33c92722cc3d
child 50698 49621c755075
     1.1 --- a/etc/options	Thu Jan 03 09:56:39 2013 +0100
     1.2 +++ b/etc/options	Thu Jan 03 13:54:45 2013 +0100
     1.3 @@ -98,3 +98,6 @@
     1.4  
     1.5  option editor_tracing_messages : int = 100
     1.6    -- "initial number of tracing messages for each command transaction"
     1.7 +
     1.8 +option editor_chart_delay : real = 3.0
     1.9 +  -- "delay for chart repainting"