| changeset 43520 | cec9b95fa35d |
| parent 43419 | 6ed49c52d463 |
| child 43661 | 39fdbd814c7f |
--- a/src/Tools/jEdit/src/output_dockable.scala Thu Jun 23 14:48:32 2011 +0200 +++ b/src/Tools/jEdit/src/output_dockable.scala Thu Jun 23 14:52:32 2011 +0200 @@ -14,6 +14,7 @@ import scala.swing.{FlowPanel, Button, CheckBox} import scala.swing.event.ButtonClicked +import java.lang.System import java.awt.BorderLayout import java.awt.event.{ComponentEvent, ComponentAdapter}