--- 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 &&