From b9c5ff1d8195dc7a419d273146769a99d95f206f Mon Sep 17 00:00:00 2001 From: "Davide P. Cervone" Date: Mon, 23 Feb 2015 12:36:51 -0500 Subject: [PATCH] Get height and depth for ALL character boxes (so large ops, etc, have correct size, since line-height kills that) --- unpacked/jax/output/CommonHTML/jax.js | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/unpacked/jax/output/CommonHTML/jax.js b/unpacked/jax/output/CommonHTML/jax.js index 0f2679b80..b6f6354e5 100644 --- a/unpacked/jax/output/CommonHTML/jax.js +++ b/unpacked/jax/output/CommonHTML/jax.js @@ -701,8 +701,8 @@ if (bbox.l === BIGDIMEN) bbox.l = 0; if (bbox.r === -BIGDIMEN) bbox.r = 0; // ### FIXME: should these be FONTDATA values? - if (bbox.h < .9) span.firstChild.style.marginTop = CHTML.Em(bbox.h-.9); - if (bbox.d < .25) span.firstChild.style.marginBottom = CHTML.Em(bbox.d-.25); + span.firstChild.style.marginTop = CHTML.Em(bbox.h-.9); + span.firstChild.style.marginBottom = CHTML.Em(bbox.d-.25); }, CHTMLbboxFor: function (n) {