Comment on dots

This follows up on 5c703aeb0397b560a383bdd57a87235834074b64.

The only reason for this change is that, subjectively, the result looks better to me. I'm not sure why, but I couldn't get used to the old symbol in spite of its seeming reasonableness. It felt really bold and heavy.

If people agree, we can wait until we need to update the screenshots for some other reason before merging this. Sorry I didn't figure this out while the discussion about the referenced commit was going on.

I'm not 100% certain how many fonts support each symbol. Please try it out and let me know if it doesn't work for you.

Compare after:

and before: