author | wenzelm |
Mon, 05 Jan 2015 14:17:17 +0100 | |
changeset 59287 | 9d4728e00925 |
parent 59286 | ac74eedb910a |
child 59288 | b1086f3e4590 |
--- a/src/Tools/Graphview/graph_panel.scala Mon Jan 05 14:13:38 2015 +0100 +++ b/src/Tools/Graphview/graph_panel.scala Mon Jan 05 14:17:17 2015 +0100 @@ -133,7 +133,7 @@ def scale_discrete: Double = { - val font_height = GUI.line_metrics(visualizer.font()).getHeight.toDouble + val font_height = GUI.line_metrics(visualizer.font()).getHeight.toInt (scale * font_height).floor / font_height }