# HG changeset patch
# User wenzelm
# Date 1467885778 -7200
# Node ID b43a3f7d99355a78f37567aec7271bed20afb789
# Parent  f473b6b16c635638bd19db1f8d29083c9e6aa353
tuned;

diff -r f473b6b16c63 -r b43a3f7d9935 src/Pure/GUI/gui.scala
--- 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