The changed text appears to be what goes in <title/> and thus didn't
help the reader much before this change. In particular, I suspect
that the prior <title/> did not help our search engine ranking much
for searches on this topic. So hopefully this change helps a bit.