src/Tools/Graphview/graph_panel.scala
changeset 59287 9d4728e00925
parent 59286 ac74eedb910a
child 59290 569a8109eeb2
--- 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
     }