# HG changeset patch
# User wenzelm
# Date 1497377965 -7200
# Node ID dcc685d5c3f7d0ed874680547c91c64a1190a73c
# Parent  2d12a730a380e38f1fdfe436b8de1e2df21fd6ff
tuned;

diff -r 2d12a730a380 -r dcc685d5c3f7 src/Tools/jEdit/src/jedit_editor.scala
--- a/src/Tools/jEdit/src/jedit_editor.scala	Tue Jun 13 20:16:39 2017 +0200
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Tue Jun 13 20:19:25 2017 +0200
@@ -16,7 +16,7 @@
 import org.gjt.sp.jedit.browser.VFSBrowser
 
 
-object JEdit_Editor extends Editor[View]
+class JEdit_Editor extends Editor[View]
 {
   /* session */
 
diff -r 2d12a730a380 -r dcc685d5c3f7 src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Tue Jun 13 20:16:39 2017 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Tue Jun 13 20:19:25 2017 +0200
@@ -56,7 +56,7 @@
   def resources: JEdit_Resources = plugin.resources
   def session: Session = plugin.session
 
-  val editor = JEdit_Editor
+  object editor extends JEdit_Editor
 }
 
 class Plugin extends EBPlugin