On Thu, Jun 28, 2018 at 09:44:13AM +0200, Magnus Hagander wrote:
> Normally I'm the biggest promoter for back-patching documentation changes
> :) But in the case when it's really just about the capitalization, I think
> it's fine to just bother with HEAD for it.
Yeah, after second-thoughts I think that I'll just fix that on HEAD
tomorrow and call it a day if there are no objections after
double-checking that no spots are missing as that's mainly cosmetic.
--
Michael