# HG changeset patch
# User wenzelm
# Date 1467964071 -7200
# Node ID 2e4de628201fae69764a2a0cc0ed07b065f139d5
# Parent  5a573668ceae139a6977abf23b6a2583f9cb6b98
tuned;

diff -r 5a573668ceae -r 2e4de628201f src/Tools/jEdit/src/jedit_lib.scala
--- a/src/Tools/jEdit/src/jedit_lib.scala	Thu Jul 07 21:58:07 2016 +0200
+++ b/src/Tools/jEdit/src/jedit_lib.scala	Fri Jul 08 09:47:51 2016 +0200
@@ -13,7 +13,6 @@
 import java.awt.event.{InputEvent, KeyEvent, KeyListener}
 import javax.swing.{Icon, ImageIcon, JWindow, SwingUtilities}
 
-import scala.annotation.tailrec
 import scala.util.parsing.input.CharSequenceReader
 
 import org.gjt.sp.jedit.{jEdit, Buffer, View, GUIUtilities, Debug, EditPane}