We were using `String.prototype.replace()` without addressing the
wrinkle that dollar signs in the replacement string have special
handling. This caused problems in situations where the replacement
string is derived from user input and contains dollar signs.
Fixes#2517