changeset 65123 | 4d088fe6185e |
parent 65107 | 70b0113fa4ef |
child 65137 | 812c35fbffa8 |
--- a/src/Tools/VSCode/etc/options Sun Mar 05 22:32:33 2017 +0100 +++ b/src/Tools/VSCode/etc/options Sun Mar 05 22:38:19 2017 +0100 @@ -1,6 +1,6 @@ (* :mode=isabelle-options: *) -option vscode_input_delay : real = 0.3 +option vscode_input_delay : real = 0.1 -- "delay for client input (edits)" option vscode_output_delay : real = 0.5