# HG changeset patch
# User wenzelm
# Date 1397514195 -7200
# Node ID c49607db182a21aea812e040f4a154fb1989739a
# Parent  f05b7d6ec5924e454f469ff627ec41ee5fe39c8d
tuned;

diff -r f05b7d6ec592 -r c49607db182a src/Tools/jEdit/src/spell_checker.scala
--- a/src/Tools/jEdit/src/spell_checker.scala	Tue Apr 15 00:21:31 2014 +0200
+++ b/src/Tools/jEdit/src/spell_checker.scala	Tue Apr 15 00:23:15 2014 +0200
@@ -21,8 +21,8 @@
 
 import org.gjt.sp.jedit.jEdit
 import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea}
-import org.gjt.sp.jedit.menu.EnhancedMenuItem;
-import org.gjt.sp.jedit.gui.DynamicContextMenuService;
+import org.gjt.sp.jedit.menu.EnhancedMenuItem
+import org.gjt.sp.jedit.gui.DynamicContextMenuService
 
 
 object Spell_Checker