# HG changeset patch
# User wenzelm
# Date 1504551306 -7200
# Node ID f6a1274be674bddb3e196d9c640c4404863b7b70
# Parent  180b2e72601fc5524b718e68364a1a2f3942bb51
tuned signature -- avoid warning during jEdit startup;

diff -r 180b2e72601f -r f6a1274be674 src/Tools/jEdit/src-base/plugin.scala
--- a/src/Tools/jEdit/src-base/plugin.scala	Mon Sep 04 15:25:25 2017 +0200
+++ b/src/Tools/jEdit/src-base/plugin.scala	Mon Sep 04 20:55:06 2017 +0200
@@ -9,7 +9,7 @@
 
 import isabelle._
 
-import org.gjt.sp.jedit.{Debug, EBPlugin}
+import org.gjt.sp.jedit.{EBMessage, Debug, EBPlugin}
 import org.gjt.sp.util.SyntaxUtilities
 
 
@@ -28,4 +28,6 @@
   {
     Syntax_Style.set_style_extender(new SyntaxUtilities.StyleExtender)
   }
+
+  override def handleMessage(message: EBMessage) { }
 }