Closed grunweg closed 3 months ago
The first paragraph is implemented in #14. The second item is easy to do, once I know a github search query for this. I have not been able to find one that works; help is welcome!
This has been implemented in #32.
Another idea for a list of things to track: "unlabelled PRs" --- PRs without an area label which should clearly have one
It may be hard (and perhaps undesirable) to label "change style detail X all over mathlib" PRs with
t-something
labels, but all feature PRs surely should be categorisable. What do you think about a list of PRs which are "features" (title starts with "feat") are do not contain a labelt-something
(i.e. whose name does not start witht-
)? Ideally, this list would be kept short; updating it is an easy chore for everybody.This list could also be extended, to PRs whose title does not start with any standard category, e.g. does not start with one of "feat", "chore", "refactor", "perf", "doc", "style" (perhaps iterating on that list).