changeset 50491 | 0faaa279faee |
parent 50478 | ccfdd1f6cf10 |
child 57035 | e865c4d99c49 |
--- a/src/Tools/Graphview/src/main_panel.scala Wed Dec 12 13:28:23 2012 +0100 +++ b/src/Tools/Graphview/src/main_panel.scala Wed Dec 12 14:54:48 2012 +0100 @@ -71,7 +71,7 @@ } } contents += Swing.RigidBox(new Dimension(10, 0)) - contents += new Library.Zoom_Box(percent => graph_panel.rescale(0.01 * percent)) + contents += graph_panel.zoom_box contents += Swing.RigidBox(new Dimension(10, 0)) contents += new Button{