src/Tools/jEdit/src-base/syntax_style.scala

--- a/src/Tools/jEdit/src-base/syntax_style.scala	Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Tools/jEdit/src-base/syntax_style.scala	Mon Mar 01 22:22:12 2021 +0100
@@ -31,11 +31,11 @@
     }
   }
 
-  def set_style_extender(extender: SyntaxUtilities.StyleExtender)
+  def set_style_extender(extender: SyntaxUtilities.StyleExtender): Unit =
   {
     SyntaxUtilities.setStyleExtender(extender)
     GUI_Thread.later { jEdit.propertiesChanged }
   }
 
-  def dummy_style_extender() { set_style_extender(Dummy_Extender) }
+  def dummy_style_extender(): Unit = set_style_extender(Dummy_Extender)
 }