--- a/src/Tools/Graphview/main_panel.scala Sat Jan 03 21:50:50 2015 +0100
+++ b/src/Tools/Graphview/main_panel.scala Sat Jan 03 22:04:31 2015 +0100
@@ -54,8 +54,8 @@
}
},
graph_panel.zoom,
+ new Button { action = Action("Fit to window") { graph_panel.fit_to_window() } },
new Button { action = Action("Apply layout") { graph_panel.apply_layout() } },
- new Button { action = Action("Fit to window") { graph_panel.fit_to_window() } },
new Button { action = Action("Colorations") { color_dialog.open } },
new Button { action = Action("Filters") { mutator_dialog.open } })