# HG changeset patch
# User wenzelm
# Date 1660299157 -7200
# Node ID bb8369922d3c4894cd4305d7c540b2cd22f87415
# Parent  d6e8d12494beef36c24cd7acddf192da45e2f49d
tuned;

diff -r d6e8d12494be -r bb8369922d3c src/Tools/jEdit/src/info_dockable.scala
--- a/src/Tools/jEdit/src/info_dockable.scala	Fri Aug 12 12:06:29 2022 +0200
+++ b/src/Tools/jEdit/src/info_dockable.scala	Fri Aug 12 12:12:37 2022 +0200
@@ -102,13 +102,13 @@
     }
 
   override def init(): Unit = {
-    GUI.parent_window(this).map(_.addWindowFocusListener(window_focus_listener))
+    GUI.parent_window(this).foreach(_.addWindowFocusListener(window_focus_listener))
     PIDE.session.global_options += main
     handle_resize()
   }
 
   override def exit(): Unit = {
-    GUI.parent_window(this).map(_.removeWindowFocusListener(window_focus_listener))
+    GUI.parent_window(this).foreach(_.removeWindowFocusListener(window_focus_listener))
     PIDE.session.global_options -= main
     delay_resize.revoke()
   }