src/Tools/jEdit/src/font_info.scala

--- a/src/Tools/jEdit/src/font_info.scala	Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Tools/jEdit/src/font_info.scala	Mon Mar 01 22:22:12 2021 +0100
@@ -40,7 +40,7 @@
 
   object main_change
   {
-    private def change_size(change: Float => Float)
+    private def change_size(change: Float => Float): Unit =
     {
       GUI_Thread.require {}
 
@@ -72,13 +72,13 @@
         })
     }
 
-    def step(i: Int)
+    def step(i: Int): Unit =
     {
       steps += i
       delay.invoke()
     }
 
-    def reset(size: Float)
+    def reset(size: Float): Unit =
     {
       delay.revoke()
       steps = 0