From 5c333a8b4777dff5dbb55d77e72b2a85406c558d Mon Sep 17 00:00:00 2001
From: "Davide P. Cervone" <dpvc@union.edu>
Date: Sun, 2 Aug 2015 17:16:15 -0400
Subject: [PATCH] Fix depth of horizontal stretchy characters to match HTML-CSS
 (should be based on extender as originally done, but font metrics don't
 really work for that with minus sign for arrows, for example).

---
 unpacked/jax/output/CommonHTML/jax.js | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

diff --git a/unpacked/jax/output/CommonHTML/jax.js b/unpacked/jax/output/CommonHTML/jax.js
index 49448536d..0cecd445c 100644
--- a/unpacked/jax/output/CommonHTML/jax.js
+++ b/unpacked/jax/output/CommonHTML/jax.js
@@ -1075,7 +1075,7 @@
       hbox.t = hbox.h; hbox.b = hbox.d;
       if (hbox.h !== ebox.h) node.style.marginTop = CHTML.Em(ebox.h - hbox.h);
       if (hbox.d !== ebox.d) node.style.marginBottom = CHTML.Em(ebox.d - hbox.d);
-      hbox.h = ebox.h; hbox.d = ebox.d;
+//      hbox.h = ebox.h; hbox.d = ebox.d;
       if (BBOX) {hbox.scale = BBOX.scale; hbox.rscale = BBOX.rscale}
       return hbox;
     },
@@ -1100,22 +1100,22 @@
         for (var i = 0, m = data[0].length; i < m; i++) text += String.fromCharCode(data[0][i]);
       } else text = String.fromCharCode(data[0]);
       if (data[4]) scale *= data[4];
-      if (scale !== 1) node.style.fontSize = this.Percent(scale);
-      var bbox = this.handleText(node,text,variant);
+      var bbox = this.handleText(node,text,variant), style = node.firstChild.style;
+      if (scale !== 1) style.fontSize = this.Percent(scale);
       if (data[2]) {  // x offset
-        node.style.paddingLeft = this.Em(data[2]);
+        style.paddingLeft = this.Em(data[2]);
         bbox.w += data[2]; bbox.r += data[2];
       }
       if (data[3]) {  // y offset
-        node.style.verticalAlign = this.Em(data[3]);
+        style.verticalAlign = this.Em(data[3]);
         bbox.h += data[3]; if (bbox.h < 0) bbox.h = 0;
       }
       if (data[5]) {  // extra height
-        node.style.marginTop = this.Em(data[5]);
+        style.marginTop = this.Em(data[5]);
         bbox.h += data[5]; bbox.t += data[5];
       }
       if (data[6]) {  // extra depth
-        node.style.marginBottom = this.Em(data[6]);
+        style.marginBottom = this.Em(data[6]);
         bbox.d += data[6]; bbox.b += data[6];
       }
       return bbox;