src/Tools/Graphview/graph_panel.scala

--- 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
     }