On Tuesday, 2 October 2012 at 23:21:13 UTC, Andrej Mitrovic wrote:
Some pull requests are rather trivial to approve and merge
(e.g. small
doc fixes, typo fixes), and it would be nice if a pull
requester could
tag a pull as "trivial" when the pull is made.
Otherwise I guess we could start using a convention and add
[trivial]
before the title? I think it might help speed up the merging
process.
It is a feature of github, but I believe was disabled. This
sounds like a good reason to enable it. Project owners?
