diff -r 5f388e514ab8 -r 77ef8bef0593 src/Tools/jEdit/src-base/jedit_lib.scala --- a/src/Tools/jEdit/src-base/jedit_lib.scala Thu Mar 04 19:55:52 2021 +0100 +++ b/src/Tools/jEdit/src-base/jedit_lib.scala Thu Mar 04 21:04:27 2021 +0100 @@ -19,7 +19,7 @@ val view = if (alt_view != null) alt_view else jEdit.getActiveView() if (view != null) { val text_area = view.getTextArea - if (text_area != null) text_area.requestFocus + if (text_area != null) text_area.requestFocus() } } } \ No newline at end of file