author | wenzelm |
Sun, 05 Mar 2017 22:38:19 +0100 | |
changeset 65123 | 4d088fe6185e |
parent 65122 | 1edb570f5b17 |
child 65124 | 759c64c39a6f |
--- 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