From 267a9a90eb81904402d8126754bc01444be4ef97 Mon Sep 17 00:00:00 2001
From: "Davide P. Cervone" <dpvc@union.edu>
Date: Wed, 14 May 2014 09:30:05 -0400
Subject: [PATCH] Use width and height attributes rather than styles.

---
 unpacked/jax/output/SVG/jax.js | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/unpacked/jax/output/SVG/jax.js b/unpacked/jax/output/SVG/jax.js
index d11bf8f74..0bb8ac894 100644
--- a/unpacked/jax/output/SVG/jax.js
+++ b/unpacked/jax/output/SVG/jax.js
@@ -2009,8 +2009,8 @@
           //
           var l = Math.max(-svg.l,0), r = Math.max(svg.r-svg.w,0);
           var style = svg.element.style;
-          style.width = SVG.Ex(l+svg.w+r);
-          style.height = SVG.Ex(svg.H+svg.D+2*SVG.em);
+          svg.element.setAttribute("width",SVG.Ex(l+svg.w+r));
+          svg.element.setAttribute("height",SVG.Ex(svg.H+svg.D+2*SVG.em));
           style.verticalAlign = SVG.Ex(-svg.D-3*SVG.em); // remove 2 extra pixels added below plus padding
           style.marginLeft = SVG.Ex(-l); style.marginRight = SVG.Ex(-r);
           svg.element.setAttribute("viewBox",(-l)+" "+(-svg.H-SVG.em)+" "+(l+svg.w+r)+" "+(svg.H+svg.D+2*SVG.em));