# HG changeset patch
# User wenzelm
# Date 1626376299 -7200
# Node ID 0f61cd0ce803f14579ee3b574be33eba9550d6ae
# Parent  f3409ced4df2eb3818631350fa6d261daa4da46d
tuned signature;

diff -r f3409ced4df2 -r 0f61cd0ce803 src/Tools/jEdit/src/main_plugin.scala
--- a/src/Tools/jEdit/src/main_plugin.scala	Thu Jul 15 21:21:16 2021 +0200
+++ b/src/Tools/jEdit/src/main_plugin.scala	Thu Jul 15 21:11:39 2021 +0200
@@ -454,7 +454,7 @@
 
       JEdit_Lib.jedit_views().foreach(init_title)
 
-      Syntax_Style.set_extender(Syntax_Style.Extender)
+      Syntax_Style.set_extender(Syntax_Style.Main_Extender)
       init_mode_provider()
       JEdit_Lib.jedit_text_areas().foreach(Completion_Popup.Text_Area.init)
 
diff -r f3409ced4df2 -r 0f61cd0ce803 src/Tools/jEdit/src/syntax_style.scala
--- a/src/Tools/jEdit/src/syntax_style.scala	Thu Jul 15 21:21:16 2021 +0200
+++ b/src/Tools/jEdit/src/syntax_style.scala	Thu Jul 15 21:11:39 2021 +0200
@@ -81,7 +81,7 @@
     }
   }
 
-  object Extender extends SyntaxUtilities.StyleExtender
+  object Main_Extender extends SyntaxUtilities.StyleExtender
   {
     val max_user_fonts = 2
     if (Symbol.font_names.length > max_user_fonts)