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] 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
         });