# HG changeset patch
# User wenzelm
# Date 1420463837 -3600
# Node ID 9d4728e0092533d729f423553d4fbc6e7f1da26b
# Parent  ac74eedb910aa3729f257a8aa53bcf666f61e702
avoid fractional font size;

diff -r ac74eedb910a -r 9d4728e00925 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
     }