On Mar 1, 2018, at 06:12, db wrote: > On 28 Feb 2018, at 14:58, Ryan Schmidt wrote: >> I wouldn't completely change the whitespace of someone else's port, even >> after a maintainer timeout. But I would correct whitespace mistakes in >> someone else's port after a suitable timeout. > > Shouldn't port lint be the rule here?
What do you mean? I don't think port lint currently gives whitespace recommendations. And if it did, port lint still just provides suggestions that must be moderated by human decisions.
