Font fixes

[dpvc]

This pull request includes fixes for a number of font issues in the 2.x milestone.

• Make U+222B (integral) stretchy in the STIX fonts (STIX-Web font data for stretchy integral is incorrect #1092)
• Remap | to variant form in STIX (that has descender) and map variant to original form (Remap | in STIX font data [was: "Bad alignement of \vert"] #1154)
• Use U+007C and U+2016 for delimiters rather than U+2223 and U+2225 (\lvert and \rvert should be to U+007C and \lVert and \rVert to U+2016 #1175)
• Fix SVG font data for stretchy characters in the TeX font data-extras files (SVG data in fontdata-extra.js is incorrect #1421)
• Alias U+2206 to U+0394 and remove incorrect U+2206 from SVG font files (SVG font data for ∆ #1418)
• Make height and depth of minus match that of plus (needed for TeX super/subscript algorithm to work properly), and adjust for that when it is used as an extender in stretchy characters (positioning of subscript or superscript minus #1187).

The last one affected all the web font files, in the HTML-CSS, SVG, and CommonHTML output, so it was extensive. This doesn't solve all the problems in the extra web font data files (there are many issues). I also didn't try to fix the scripts that were used originally to create the files, as I didn't want to waste time on that, as I think the whole web font approach needs to be rethought for v3.0. So these were edited by hand (we'll need to remember that for the future).

[zorkow]

I did not really understand what is going on... but I assume it works.

[dpvc]

Yes, I think it does. If not, I'm hoping the test suite will catch it. So I will merge for now.