Apparently some web server setups may serve this file in a different encoding
than UTF-8, and that results in visual garbage in the followlines button that
renders for every line in a file. So instead of using this Unicode character in
UTF-8 we can encode it as \u2212. Or, to be more explicit, we can use −
HTML entity, which resolves into exactly that character.
Since now we're using innerHTML property to set the minus part of the button,
let's use it to set the plus part as well (even though the plus sign was plain
ASCII). A wise man once said "A foolish consistency is the hobgob... eh,
whatever." Throw a brick at me if this makes things worse.