src/Tools/Graphview/mutator_dialog.scala
changeset 59391 39a38657d16b
parent 59246 32903b99c2ef
child 59459 985fc55e9f27
--- a/src/Tools/Graphview/mutator_dialog.scala	Sun Jan 18 17:31:27 2015 +0100
+++ b/src/Tools/Graphview/mutator_dialog.scala	Sun Jan 18 17:32:38 2015 +0100
@@ -155,8 +155,8 @@
   contents = new BorderPanel {
     border = new EmptyBorder(5, 5, 5, 5)
 
-    add(new ScrollPane(filter_panel), BorderPanel.Position.Center)
-    add(botPanel, BorderPanel.Position.South)
+    layout(new ScrollPane(filter_panel)) = BorderPanel.Position.Center
+    layout(botPanel) = BorderPanel.Position.South
   }
 
   private class Mutator_Panel(initials: Mutator.Info)