Remap U+2016 to U+2225 in normal and bold TeX fonts, now that \|
produces U+2016 rather than U+2225, and U+2016 isn't in MAIN font. Resolves issue #1610 (closed).
Remap U+2016 to U+2225 in normal and bold TeX fonts, now that \|
produces U+2016 rather than U+2225, and U+2016 isn't in MAIN font. Resolves issue #1610 (closed).