www

commit efb24b7fc281546bc06edd45291db42196ba1861
parent d127b1bcb73bcefc59c167c84aaadee0847f893d
Author: Davide P. Cervone <dpvc@union.edu>
Date:   Mon, 20 Jul 2015 11:33:27 -0400

Properly detect the extra web fonts in IE10+.  Resolves issue #1211.

Diffstat:
M
unpacked/jax/output/HTML-CSS/jax.js
 | 
3
++-

1 file changed, 2 insertions(+), 1 deletion(-)
diff --git a/unpacked/jax/output/HTML-CSS/jax.js b/unpacked/jax/output/HTML-CSS/jax.js
@@ -103,7 +103,7 @@
       //  This should be removed when the web fonts are fixed.  FIXME
       //
       var family = font.familyFixed || font.family;
-      if (!family.match(/^(STIX|MathJax)|'/)) {
+      if (!font.isWebFont && !family.match(/^(STIX|MathJax)|'/)) {
         family = family.replace(/_/g," ").replace(/([a-z])([A-Z])/g,"$1 $2").replace(/ Jax/,"Jax")
                + "','" + family + "','" + family + "-";
         if (font.weight) {family += "Bold"}; if (font.style) {family += "Italic"}
@@ -213,6 +213,7 @@
       var type = HTMLCSS.allowWebFonts;
       var FONT = HTMLCSS.FONTDATA.FONTS[name];
       if (HTMLCSS.msieFontCSSBug && !FONT.family.match(/-Web$/)) {FONT.family += "-Web"}
+      if (FONT.isWebFont) delete FONT.familyFixed;
       var webfonts = HTMLCSS.webfontDir+"/"+type;
       var dir = AJAX.fileURL(webfonts);
       var fullname = name.replace(/-b/,"-B").replace(/-i/,"-I").replace(/-Bold-/,"-Bold");