diff --git a/unpacked/jax/output/HTML-CSS/fonts/STIX-Web/fontdata-extra.js b/unpacked/jax/output/HTML-CSS/fonts/STIX-Web/fontdata-extra.js index 210b014d4..e7f77b4f4 100644 --- a/unpacked/jax/output/HTML-CSS/fonts/STIX-Web/fontdata-extra.js +++ b/unpacked/jax/output/HTML-CSS/fonts/STIX-Web/fontdata-extra.js @@ -415,9 +415,9 @@ }, 0x222B: { - dir: H, + dir: V, HW: [[0.607,MAIN], [0.979,SIZE1]], - stretch: {top:[0xE03C,SIZE5], rep:[0xE03D,SIZE5], bot:[0xE03E,SIZE5]} + stretch: {top:[0xE03C,SIZE5], ext:[0xE03D,SIZE5], bot:[0xE03E,SIZE5]} }, 0x222C: { diff --git a/unpacked/jax/output/HTML-CSS/fonts/STIX-Web/fontdata.js b/unpacked/jax/output/HTML-CSS/fonts/STIX-Web/fontdata.js index 461cd2f44..2909f8cb4 100644 --- a/unpacked/jax/output/HTML-CSS/fonts/STIX-Web/fontdata.js +++ b/unpacked/jax/output/HTML-CSS/fonts/STIX-Web/fontdata.js @@ -531,7 +531,7 @@ HW: [[0.879,MAIN]], stretch: {ext:[0x2225,MAIN]} }, - 0x222B: EXTRAH, + 0x222B: EXTRAV, 0x222C: EXTRAV, 0x222D: EXTRAV, 0x222E: EXTRAV, diff --git a/unpacked/jax/output/HTML-CSS/fonts/STIX/fontdata-extra.js b/unpacked/jax/output/HTML-CSS/fonts/STIX/fontdata-extra.js index ed0a16bd4..3c101e9b7 100644 --- a/unpacked/jax/output/HTML-CSS/fonts/STIX/fontdata-extra.js +++ b/unpacked/jax/output/HTML-CSS/fonts/STIX/fontdata-extra.js @@ -37,7 +37,8 @@ SIZE2 = "STIXSizeTwoSym", SIZE3 = "STIXSizeThreeSym", SIZE4 = "STIXSizeFourSym", - SIZE5 = "STIXSizeFiveSym"; + SIZE5 = "STIXSizeFiveSym", + INTD = "STIXIntegralsD"; var H = "H", V = "V"; var delim = { @@ -121,6 +122,11 @@ { dir: H, HW: [[.926,GENERAL]], stretch: {right:[0x21DB,GENERAL], rep:[0x2261,GENERAL]} }, + 0x222B: // integral + { + dir: V, HW: [[0.607,GENERAL], [0.979,INTD]], + stretch: {top:[0x2320,SIZE1], ext:[0x23AE,SIZE1], bot:[0x2321,SIZE1]} + }, 0x23B4: // top square bracket { dir: H, HW: [[.926,GENERAL],[1.063,SIZE1],[1.606,SIZE2],[2.147,SIZE3],[2.692,SIZE4],[3.237,SIZE5]], diff --git a/unpacked/jax/output/HTML-CSS/fonts/STIX/fontdata.js b/unpacked/jax/output/HTML-CSS/fonts/STIX/fontdata.js index 920de949a..5643f987e 100644 --- a/unpacked/jax/output/HTML-CSS/fonts/STIX/fontdata.js +++ b/unpacked/jax/output/HTML-CSS/fonts/STIX/fontdata.js @@ -406,6 +406,7 @@ 0x21C3: EXTRAV, // down harpoon with barb left 0x21DA: EXTRAH, // left triple arrow 0x21DB: EXTRAH, // right triple arrow + 0x222B: EXTRAV, // integral 0x23B4: EXTRAH, // top square bracket 0x23B5: EXTRAH, // bottom square bracket 0x23DC: EXTRAH, // top paren diff --git a/unpacked/jax/output/SVG/fonts/STIX-Web/fontdata-extra.js b/unpacked/jax/output/SVG/fonts/STIX-Web/fontdata-extra.js index 75280f595..44bb64fd7 100644 --- a/unpacked/jax/output/SVG/fonts/STIX-Web/fontdata-extra.js +++ b/unpacked/jax/output/SVG/fonts/STIX-Web/fontdata-extra.js @@ -415,9 +415,9 @@ }, 0x222B: { - dir: H, + dir: V, HW: [[607,MAIN], [979,SIZE1]], - stretch: {top:[0xE03C,SIZE5], rep:[0xE03D,SIZE5], bot:[0xE03E,SIZE5]} + stretch: {top:[0xE03C,SIZE5], ext:[0xE03D,SIZE5], bot:[0xE03E,SIZE5]} }, 0x222C: { diff --git a/unpacked/jax/output/SVG/fonts/STIX-Web/fontdata.js b/unpacked/jax/output/SVG/fonts/STIX-Web/fontdata.js index a2a26eb45..05c62ba6e 100644 --- a/unpacked/jax/output/SVG/fonts/STIX-Web/fontdata.js +++ b/unpacked/jax/output/SVG/fonts/STIX-Web/fontdata.js @@ -528,7 +528,7 @@ HW: [[879,MAIN]], stretch: {ext:[0x2225,MAIN]} }, - 0x222B: EXTRAH, + 0x222B: EXTRAV, 0x222C: EXTRAV, 0x222D: EXTRAV, 0x222E: EXTRAV,