patch 8.2.1913: GTK GUI: rounding for the cell height is too strict

Problem:    GTK GUI: rounding for the cell height is too strict.
Solution:   Round up above 15/16 of a pixel. (closes #7203)

diff --git a/src/gui_gtk_x11.c b/src/gui_gtk_x11.c
index 2c5864ed4a50be46f4b6fa6abc5268149eca2e91..1a4ebf9ba6b41489fde04727bd0cbfe5db868a32 100644 (file)
--- a/src/gui_gtk_x11.c
+++ b/src/gui_gtk_x11.c
@@ -4726,9 +4726,10 @@ gui_mch_adjust_charheight(void)
 
     pango_font_metrics_unref(metrics);
 
-    // Round up, but not when the value is very close (e.g. 15.0009).
-    gui.char_height = (ascent + descent + PANGO_SCALE - 3) / PANGO_SCALE
-                                                               + p_linespace;
+    // Round up when the value is more than about 1/16 of a pixel above a whole
+    // pixel (12.0624 becomes 12, 12.07 becomes 13).  Then add 'linespace'.
+    gui.char_height = (ascent + descent + (PANGO_SCALE * 15) / 16)
+                                                  / PANGO_SCALE + p_linespace;
     // LINTED: avoid warning: bitwise operation on signed value
     gui.char_ascent = PANGO_PIXELS(ascent + p_linespace * PANGO_SCALE / 2);
 

diff --git a/src/version.c b/src/version.c
index adef583b9192acad31489862a57929a021481049..b83bc48112f3a9142e5a44b8ef46f6a9839a1a0f 100644 (file)
--- a/src/version.c
+++ b/src/version.c
@@ -750,6 +750,8 @@ static char *(features[]) =
 
 static int included_patches[] =
 {   /* Add new patch number below this line */
+/**/
+    1913,
 /**/
     1912,
 /**/