www

commit b9c5ff1d8195dc7a419d273146769a99d95f206f
parent 8f0e833ba62d749f6b5f1a3cab08204d8534caab
Author: Davide P. Cervone <dpvc@union.edu>
Date:   Mon, 23 Feb 2015 12:36:51 -0500

Get height and depth for ALL character boxes (so large ops, etc, have correct size, since line-height kills that)

Diffstat:
M
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
@@ -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) {