Minor tweak as a side effect of fixing #1243553. The Unicode name for " is

'quotation mark', so I decided to use it instead of 'double-quote'.