On Thu, Nov 22, 2018 at 10:34:56AM -0500, Shreyans Devendra Doshi wrote: > Fixes a spelling error and removes an extra whitespace character. There is a fierce battle amongst those who insist on one space after a full stop and those who insist on two. I recommend not getting caught up in this battle, particularly since the point of this is to produce html documentation and the amount of space displayed after a period is then up to your web browser, not the source text. I would not NACK this patch, since it does fix a typo, but please don't send any more patches which adjust the number of whitespaces after a full stop.
