From 8eb029478e6fb94976dc05959f54ecee7d0583cb Mon Sep 17 00:00:00 2001
From: "Davide P. Cervone" <dpvc@union.edu>
Date: Fri, 30 May 2014 12:15:25 -0400
Subject: [PATCH 1/2] Fix bounding box problem in Firefox with stretchy
 delimiters (and remove alignment hack that doesn't seem to be needed any
 longer).  resolves issue #729.

---
 unpacked/jax/output/HTML-CSS/jax.js | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/unpacked/jax/output/HTML-CSS/jax.js b/unpacked/jax/output/HTML-CSS/jax.js
index 2d103ac77..22e51d40b 100644
--- a/unpacked/jax/output/HTML-CSS/jax.js
+++ b/unpacked/jax/output/HTML-CSS/jax.js
@@ -1392,7 +1392,10 @@
           span.style.top = this.Em(-h);
         } else {
           span.style.verticalAlign = this.Em(h);
-          if (HTMLCSS.ffVerticalAlignBug) {HTMLCSS.createRule(span.parentNode,span.bbox.h,0,0)}
+	  if (HTMLCSS.ffVerticalAlignBug) {
+	    HTMLCSS.createRule(span.parentNode,span.bbox.h,0,0);
+	    delete span.parentNode.bbox;
+	  }
         }
       }
     },
@@ -2934,7 +2937,7 @@
               (HUB.config.root+"/").substr(0,root.length) === root) {webFonts = "otf"}
         }
         HTMLCSS.Augment({
-          ffVerticalAlignBug: true,
+          ffVerticalAlignBug: !browser.versionAtLeast("20.0"),  // not sure when this bug was fixed
           AccentBug: true,
           allowWebFonts: webFonts
         });

From 668585f5912f500a68f752e8260c854bde9c5d51 Mon Sep 17 00:00:00 2001
From: "Davide P. Cervone" <dpvc@union.edu>
Date: Fri, 30 May 2014 12:17:09 -0400
Subject: [PATCH 2/2] Fix several problems with stretchy delimiters in SVG
 output (minsize didn't always get processed, stretched characters weren't
 marked as such).

---
 unpacked/jax/output/SVG/jax.js | 15 ++++++++++++---
 1 file changed, 12 insertions(+), 3 deletions(-)

diff --git a/unpacked/jax/output/SVG/jax.js b/unpacked/jax/output/SVG/jax.js
index db1b57732..396c1e8ad 100644
--- a/unpacked/jax/output/SVG/jax.js
+++ b/unpacked/jax/output/SVG/jax.js
@@ -1325,8 +1325,15 @@
       },
       
       SVGcanStretch: function (direction) {
-	if (this.isEmbellished()) {return this.Core().SVGcanStretch(direction)}
-	return false;
+        var can = false;
+	if (this.isEmbellished()) {
+          var core = this.Core();
+          if (core && core !== this) {
+            can = core.SVGcanStretch(direction);
+            if (can && core.forceStretch) {this.forceStretch = true}
+          }
+        }
+        return can;
       },
       SVGstretchV: function (h,d) {return this.toSVG(h,d)},
       SVGstretchH: function (w) {return this.toSVG(w)},
@@ -1425,7 +1432,7 @@
       CoreParent: function () {
         var parent = this;
         while (parent && parent.isEmbellished() &&
-               parent.CoreMO() === this && !parent.isa(MML.math))  {parent = parent.Parent()}
+               parent.CoreMO() === this && !parent.isa(MML.math)) {parent = parent.Parent()}
         return parent;
       },
       CoreText: function (parent) {
@@ -1486,6 +1493,7 @@
 	this.SVGhandleColor(svg);
         delete this.svg.element;
         this.SVGsaveData(svg);
+        svg.stretched = true;
 	return svg;
       },
       SVGstretchH: function (w) {
@@ -1502,6 +1510,7 @@
 	this.SVGhandleColor(svg);
         delete this.svg.element;
         this.SVGsaveData(svg);
+        svg.stretched = true;
 	return svg;
       }
     });