# HG changeset patch
# User wenzelm
# Date 1730978796 -3600
# Node ID 6cb5ac3096fad2ab1f18ad11b9b8bf49c698c1b9
# Parent  75a2c6af8a026bdc2cb08988231f0d3b750de088
tuned;

diff -r 75a2c6af8a02 -r 6cb5ac3096fa src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Thu Nov 07 12:17:18 2024 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Thu Nov 07 12:26:36 2024 +0100
@@ -115,9 +115,7 @@
     }
   }
 
-  def resize(font_info: Font_Info): Unit = {
-    GUI_Thread.require {}
-
+  def resize(font_info: Font_Info): Unit = GUI_Thread.require {
     current_font_info = font_info
     refresh()
   }