Redo commit 7244ae9a.  The same trivial change was done with an online edit, but this resulted in some corruption of special characters in the file, likely because of differences with the character set used by the Bitbucket online editor.