changeset 69898 | 990c6e8faf2c |
parent 69256 | c78c95d2a3d1 |
child 70302 | 9ea7081c3f03 |
--- a/src/Tools/VSCode/src/vscode_rendering.scala Mon Mar 11 16:47:22 2019 +0100 +++ b/src/Tools/VSCode/src/vscode_rendering.scala Mon Mar 11 18:58:06 2019 +0100 @@ -247,7 +247,7 @@ /* tooltips */ - def timing_threshold: Double = options.real("vscode_timing_threshold") + override def timing_threshold: Double = options.real("vscode_timing_threshold") /* hyperlinks */