diff --git a/src/display/update_lines.js b/src/display/update_lines.js index 095cddef3f3348671a51c24b0dd4081d1a553f32..7583f3c15988cfb22a91d9dd5d18038c5b755f2d 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++)