-- (U+00A0).
{symbol = ' ', repr = ' '},
{symbol = '_', repr = '\\_'},
+ {symbol = '->>', repr = '\\twoheadrightarrow'},
{symbol = '->', repr = '→'},
{symbol = '=>', repr = '⇒'},
-- The default * sits very high above the baseline, \ast (u+2217) looks