Thread titles with user pings show @numbers

[cellio]

meta:289223

If a thread title -- the first hundred or so characters of the comment, if there's no explicit title -- contains a user ping, that ping is properly translated into the user name in the comment, but not in the thread title. If it's easy to also insert the name into the title, let's do that. If not, let's do something else to make thread titles not ugly. I'm not sure what "something else" should be; at the beginning of the line we could just strip it, but that would make a mess if a comment begins with something like "The answer by @1234 points out that...". Before we worry about that: is it easy to show the name in the title and avoid the problem?