--- a/src/Tools/Graphview/graph_panel.scala Tue Jun 27 20:16:40 2017 +0200
+++ b/src/Tools/Graphview/graph_panel.scala Tue Jun 27 21:36:58 2017 +0200
@@ -345,8 +345,10 @@
private val filters = new Button { action = Action("Filters") { mutator_dialog.open } }
private val controls =
- new Wrap_Panel(Wrap_Panel.Alignment.Right)(show_content, show_arrow_heads, show_dummies,
- save_image, zoom, fit_window, update_layout, editor_style) // FIXME colorations, filters
+ Wrap_Panel(
+ List(show_content, show_arrow_heads, show_dummies,
+ save_image, zoom, fit_window, update_layout, editor_style), // FIXME colorations, filters
+ Wrap_Panel.Alignment.Right)