Make About box show 'woff or otf' when otf fonts are used (since both are requested).

Author: dpvc

unpacked/extensions/MathMenu.js

@@ -607,7 +607,8 @@
     MENU.About.GetJax(jax,MathJax.Extension,"Extension",true);
     jax.push(["div",{style:{"border-top":"groove 2px",margin:".25em 0"}}],["center",{},[
       HUB.Browser + " v"+HUB.Browser.version +
-      (HTMLCSS.webFonts && !HTMLCSS.imgFonts ? " \u2014 "+HTMLCSS.allowWebFonts+" fonts" : "")
+      (HTMLCSS.webFonts && !HTMLCSS.imgFonts ? " \u2014 " + 
+        HTMLCSS.allowWebFonts.replace(/otf/,"woff or otf") + " fonts" : "")
     ]]);
     MENU.About.div = MENU.Background(MENU.About);
     var about = HTML.addElement(MENU.About.div,"div",{