etc/options
changeset 64524 e6a3c55b929b
parent 64325 47e03cb99274
child 65056 002b4c8c366e
     1.1 --- a/etc/options	Thu Nov 24 11:33:55 2016 +0100
     1.2 +++ b/etc/options	Thu Nov 24 15:21:54 2016 +0100
     1.3 @@ -144,6 +144,9 @@
     1.4  public option editor_input_delay : real = 0.3
     1.5    -- "delay for user input (text edits, cursor movement etc.)"
     1.6  
     1.7 +public option editor_generated_input_delay : real = 1.0
     1.8 +  -- "delay for machine-generated input that may outperform user edits"
     1.9 +
    1.10  public option editor_output_delay : real = 0.1
    1.11    -- "delay for prover output (markup, common messages etc.)"
    1.12