// European Number Terminators: percent, permille, degree, euro etc.
if (cur.current_font.fontInfo().number() == FONT_ON) {
if (!isDigitASCII(c) && !contains(number_operators, c) &&
// European Number Terminators: percent, permille, degree, euro etc.
if (cur.current_font.fontInfo().number() == FONT_ON) {
if (!isDigitASCII(c) && !contains(number_operators, c) &&