Fix stretch data for U+222B (integral) in STIX-Web data for HTML-CSS and SVG, and add it so local STIX data. Resolves issue mathjax#1092.

Author: dpvc

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:
       {

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,

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]],

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

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:
       {

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,