changeset 71601 | 97ccf48c2f0c |
parent 71383 | 8313dca6dee9 |
child 73340 | 0ffcad1f6130 |
--- a/src/Tools/Graphview/mutator_dialog.scala Fri Mar 27 13:04:15 2020 +0100 +++ b/src/Tools/Graphview/mutator_dialog.scala Fri Mar 27 22:01:27 2020 +0100 @@ -110,7 +110,7 @@ filter_panel.repaint } - val filter_panel = new BoxPanel(Orientation.Vertical) {} + val filter_panel: BoxPanel = new BoxPanel(Orientation.Vertical) {} private val mutator_box = new ComboBox[Mutator](container.available)