diff -r 9efdebe24c65 -r 0ffcad1f6130 src/Tools/jEdit/src-base/jedit_lib.scala
--- a/src/Tools/jEdit/src-base/jedit_lib.scala	Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Tools/jEdit/src-base/jedit_lib.scala	Mon Mar 01 22:22:12 2021 +0100
@@ -14,7 +14,7 @@
 
 object JEdit_Lib
 {
-  def request_focus_view(alt_view: View = null)
+  def request_focus_view(alt_view: View = null): Unit =
   {
     val view = if (alt_view != null) alt_view else jEdit.getActiveView()
     if (view != null) {