I find [PROPOSAL] and all other title tags redundant and prefer the github labels since they are easier to use for searching, and would prefer the tags in the title were not there. I guess I don't mind [Backport] as much because it makes it really stand out that it's a PR for backporting for release, but it is also probably not necessary if we just want to get rid of them entirely. I feel the same about putting the issue number in the PR title, which is also pretty worthless since it doesn't link it.
A bot to automatically do that might be nice, +1. I wonder how much work it would be to examine which paths are modified by a PR to attempt to automatically add 'Area' labels too, but that might be overkill. On Thu, Mar 14, 2019 at 2:36 PM Roman Leventov <[email protected]> wrote: > 1) Do other people want proposal issues to have [PROPOSAL] in their names, > despite they also have a corresponding tag? Maybe we can at least make it > not caps? > > 2) Would be nice to teach bot to visit PRs and issues from non-committers > and remove "[tag name]" parts from their titles and assign corresponding > tags. >
