# 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