# HG changeset patch
# User wenzelm
# Date 1274560243 -7200
# Node ID 7d796b72099f1937b0acba6437e5eea532a4d5b1
# Parent  07936a4efe938ff19dfe105d0f77a00a2e89a304
tuned;

diff -r 07936a4efe93 -r 7d796b72099f src/Tools/jEdit/src/jedit/html_panel.scala
--- a/src/Tools/jEdit/src/jedit/html_panel.scala	Sat May 22 22:30:37 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/html_panel.scala	Sat May 22 22:30:43 2010 +0200
@@ -13,7 +13,6 @@
 import java.awt.{BorderLayout, Dimension, GraphicsEnvironment, Toolkit, FontMetrics}
 import java.awt.event.MouseEvent
 
-import javax.swing.{JButton, JPanel, JScrollPane}
 import java.util.logging.{Logger, Level}
 
 import org.w3c.dom.html2.HTMLElement