# HG changeset patch
# User wenzelm
# Date 1731580431 -3600
# Node ID 82110cbcf9a1d0874cbceaa4a72a0aa01108a623
# Parent  cd685e2291faa02cd8bb9de2574cbb73aa34f95f
disable 2d9b6e32632d for now: unknown problems on macOS;

diff -r cd685e2291fa -r 82110cbcf9a1 src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Thu Nov 14 11:12:11 2024 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Thu Nov 14 11:33:51 2024 +0100
@@ -111,7 +111,8 @@
           GUI_Thread.later {
             val current_metric = JEdit_Lib.font_metric(getPainter)
             val current_margin = Rich_Text.component_margin(current_metric, getPainter)
-            if (metric == current_metric &&
+            if (true || // FIXME
+                metric == current_metric &&
                 margin == current_margin &&
                 output == current_output &&
                 snapshot == current_base_snapshot &&