| changeset 64727 | 13e37567a0d6 |
| parent 64684 | fe2c9c215b36 |
| child 64870 | 41e2797af496 |
--- a/src/Tools/VSCode/etc/options Sat Dec 31 15:32:54 2016 +0100 +++ b/src/Tools/VSCode/etc/options Sat Dec 31 20:26:34 2016 +0100 @@ -6,6 +6,9 @@ option vscode_output_delay : real = 0.5 -- "delay for client output (rendering)" +option vscode_load_delay : real = 0.5 + -- "delay for file load operations" + option vscode_tooltip_margin : int = 60 -- "margin for pretty-printing of tooltips"