changeset 71383 | 8313dca6dee9 |
parent 66206 | 2d2082db735a |
child 73340 | 0ffcad1f6130 |
--- a/src/Tools/Graphview/graph_panel.scala Wed Jan 15 19:49:13 2020 +0100 +++ b/src/Tools/Graphview/graph_panel.scala Wed Jan 15 19:54:50 2020 +0100 @@ -148,7 +148,7 @@ (scale * font_height).floor / font_height } - def apply() = + def apply(): AffineTransform = { val box = graphview.bounding_box() val t = AffineTransform.getScaleInstance(scale_discrete, scale_discrete)