--- 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)