src/Tools/Graphview/main_panel.scala
changeset 59302 4d985afc0565
parent 59294 126293918a37
child 59384 c75327a34960
     1.1 --- a/src/Tools/Graphview/main_panel.scala	Mon Jan 05 23:29:38 2015 +0100
     1.2 +++ b/src/Tools/Graphview/main_panel.scala	Tue Jan 06 16:33:30 2015 +0100
     1.3 @@ -66,7 +66,7 @@
     1.4  
     1.5    private def export(file: JFile)
     1.6    {
     1.7 -    val box = visualizer.Coordinates.bounding_box()
     1.8 +    val box = visualizer.bounding_box()
     1.9      val w = box.width.ceil.toInt
    1.10      val h = box.height.ceil.toInt
    1.11