Provide API to double a char in a string

Yes there is someString.replace("a", "aa"); but I want something as fast as possible for a very repetitive task in this case (11000 calls that takes 12% of the time when viewing an empty page in XE).

Here the result of some benchmarks I did before creating doing it:

• about 3 times quicker when there is something to do (whatever you do around it most of the time is taken by StringBuilder operations in practice but 3 is already nice)
• about 30 times quicker when there is nothing to do (which is about 99% of the time in our case)