Issue #12728: Different Unicode characters having the same uppercase but

different lowercase are now matched in case-insensitive regular expressions.