| changeset 63420 | b43a3f7d9935 |
| parent 62113 | 16de2a9b5b3d |
| child 63874 | e2393cfde472 |
--- a/src/Pure/GUI/gui.scala Thu Jul 07 11:46:18 2016 +0200 +++ b/src/Pure/GUI/gui.scala Thu Jul 07 12:02:58 2016 +0200 @@ -15,7 +15,6 @@ import javax.swing.{ImageIcon, JOptionPane, UIManager, JLayeredPane, JFrame, JWindow, JDialog, JButton, JTextField} -import scala.collection.convert.WrapAsJava import scala.swing.{ComboBox, TextArea, ScrollPane} import scala.swing.event.SelectionChanged