src/Tools/Graphview/mutator_dialog.scala
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)