src/Tools/VSCode/src/vscode_rendering.scala
changeset 70079 990c6e8faf2c
parent 69261 c78c95d2a3d1
     1.1 --- a/src/Tools/VSCode/src/vscode_rendering.scala	Mon Mar 11 16:47:22 2019 +0100
     1.2 +++ b/src/Tools/VSCode/src/vscode_rendering.scala	Mon Mar 11 18:58:06 2019 +0100
     1.3 @@ -247,7 +247,7 @@
     1.4  
     1.5    /* tooltips */
     1.6  
     1.7 -  def timing_threshold: Double = options.real("vscode_timing_threshold")
     1.8 +  override def timing_threshold: Double = options.real("vscode_timing_threshold")
     1.9  
    1.10  
    1.11    /* hyperlinks */