From 449eab87b3753c5ec1c16dbaab44484366da76e6 Mon Sep 17 00:00:00 2001
From: Simon Edwards <simon@simonzone.com>
Date: Wed, 28 Jun 2017 07:03:55 +0200
Subject: [PATCH] Make line height calculations more tolerant of browser
rounding errors
---
src/display/update_lines.js | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/src/display/update_lines.js b/src/display/update_lines.js
index 095cddef..7583f3c1 100644
--- a/src/display/update_lines.js
+++ b/src/display/update_lines.js
@@ -21,7 +21,7 @@ export function updateHeightsInViewport(cm) {
}
let diff = cur.line.height - height
if (height < 2) height = textHeight(display)
- if (diff > .001 || diff < -.001) {
+ if (diff > .005 || diff < -.005) {
updateLineHeight(cur.line, height)
updateWidgetHeight(cur.line)
if (cur.rest) for (let j = 0; j < cur.rest.length; j++)
--
GitLab