Merge pull request #1612 from dpvc/issue1610

Use proper glyph for \| in TeX fonts (in HTML-CSS, CHTML, and SVG).  #1610

Author: dpvc

jax/output/CommonHTML/fonts/TeX/fontdata.js

@@ -95,6 +95,7 @@
                  remap: {0x391:0x41, 0x392:0x42, 0x395:0x45, 0x396:0x5A, 0x397:0x48,
                          0x399:0x49, 0x39A:0x4B, 0x39C:0x4D, 0x39D:0x4E, 0x39F:0x4F,
                          0x3A1:0x50, 0x3A4:0x54, 0x3A7:0x58,
+                         0x2016:0x2225,
                          0x2216:[0x2216,"-TeX-variant"],  // \smallsetminus
                          0x210F:[0x210F,"-TeX-variant"],  // \hbar
                          0x2032:[0x27,"sans-serif-italic"],  // HACK: a smaller prime
@@ -104,6 +105,7 @@
                  remap: {0x391:0x41, 0x392:0x42, 0x395:0x45, 0x396:0x5A, 0x397:0x48,
                          0x399:0x49, 0x39A:0x4B, 0x39C:0x4D, 0x39D:0x4E, 0x39F:0x4F,
                          0x3A1:0x50, 0x3A4:0x54, 0x3A7:0x58, 0x29F8:[0x002F,"bold-italic"],
+                         0x2016:0x2225,
                          0x219A:"\u2190\u0338", 0x219B:"\u2192\u0338", 0x21AE:"\u2194\u0338",
                          0x21CD:"\u21D0\u0338", 0x21CE:"\u21D4\u0338", 0x21CF:"\u21D2\u0338",
                          0x2204:"\u2203\u0338", 0x2224:"\u2223\u0338", 0x2226:"\u2225\u0338",

jax/output/HTML-CSS/fonts/TeX/fontdata.js

@@ -78,6 +78,7 @@
                    remap: {0x391:0x41, 0x392:0x42, 0x395:0x45, 0x396:0x5A, 0x397:0x48,
                            0x399:0x49, 0x39A:0x4B, 0x39C:0x4D, 0x39D:0x4E, 0x39F:0x4F,
                            0x3A1:0x50, 0x3A4:0x54, 0x3A7:0x58,
+                           0x2016:0x2225,
                            0x2216:[0x2216,"-TeX-variant"],  // \smallsetminus
                            0x210F:[0x210F,"-TeX-variant"],  // \hbar
                            0x2032:[0x27,"sans-serif-italic"],  // HACK: a smaller prime
@@ -87,6 +88,7 @@
                    remap: {0x391:0x41, 0x392:0x42, 0x395:0x45, 0x396:0x5A, 0x397:0x48,
                            0x399:0x49, 0x39A:0x4B, 0x39C:0x4D, 0x39D:0x4E, 0x39F:0x4F,
                            0x3A1:0x50, 0x3A4:0x54, 0x3A7:0x58, 0x29F8:[0x002F,"bold-italic"],
+                           0x2016:0x2225,
                            0x219A:"\u2190\u0338", 0x219B:"\u2192\u0338", 0x21AE:"\u2194\u0338",
                            0x21CD:"\u21D0\u0338", 0x21CE:"\u21D4\u0338", 0x21CF:"\u21D2\u0338",
                            0x2204:"\u2203\u0338", 0x2224:"\u2223\u0338", 0x2226:"\u2225\u0338",

jax/output/SVG/fonts/TeX/fontdata.js

@@ -76,6 +76,7 @@
                    remap: {0x391:0x41, 0x392:0x42, 0x395:0x45, 0x396:0x5A, 0x397:0x48,
                            0x399:0x49, 0x39A:0x4B, 0x39C:0x4D, 0x39D:0x4E, 0x39F:0x4F,
                            0x3A1:0x50, 0x3A4:0x54, 0x3A7:0x58,
+                           0x2016:0x2225,
                            0x2216:[0x2216,"-TeX-variant"],  // \smallsetminus
                            0x210F:[0x210F,"-TeX-variant"],  // \hbar
                            0x2032:[0x27,"sans-serif-italic"],  // HACK: a smaller prime
@@ -85,6 +86,7 @@
                    remap: {0x391:0x41, 0x392:0x42, 0x395:0x45, 0x396:0x5A, 0x397:0x48,
                            0x399:0x49, 0x39A:0x4B, 0x39C:0x4D, 0x39D:0x4E, 0x39F:0x4F,
                            0x3A1:0x50, 0x3A4:0x54, 0x3A7:0x58, 0x29F8:[0x002F,"bold-italic"],
+                           0x2016:0x2225,
                            0x219A:"\u2190\u0338", 0x219B:"\u2192\u0338", 0x21AE:"\u2194\u0338",
                            0x21CD:"\u21D0\u0338", 0x21CE:"\u21D4\u0338", 0x21CF:"\u21D2\u0338",
                            0x2204:"\u2203\u0338", 0x2224:"\u2223\u0338", 0x2226:"\u2225\u0338",