Hello, Is somebody fundamentally opposing the idea of applying labels to pull requests when applicable? I went through the pull requests and it would be nice to have some basic filters, like "show me all pull requests related to documentation" would be labeled as "docs", then PRs fixing some tests would be "tests" and so on. We may further narrow it down for subsystems etc.
I do not mind applying myself in this to tag the PRs as they come if people do not tag it themselves in order to have at least some basic "filterability". As I went through PRs closing already committed ones, I noticed there are a lot of PRs related to documentation which just tend to be completely forgotten in the long run. Does this make sense to people? Regards Stefan
