author | wenzelm |
Mon, 19 Jan 2015 21:06:47 +0100 | |
changeset 59411 | 99d009ede619 |
parent 59410 | 19f396384cbe |
child 59412 | 0426b53a5d54 |
--- a/src/Tools/Graphview/graph_panel.scala Mon Jan 19 21:06:01 2015 +0100 +++ b/src/Tools/Graphview/graph_panel.scala Mon Jan 19 21:06:47 2015 +0100 @@ -333,7 +333,7 @@ private val controls = new Wrap_Panel(Wrap_Panel.Alignment.Right)(show_content, show_arrow_heads, show_dummies, - save_image, zoom, fit_window, update_layout, colorations, filters) + save_image, zoom, fit_window, update_layout) // FIXME colorations, filters /* save file */