I don't really know how to manage GitHub notifications. It feels like I'm either:
1. "Watching" the repository I work on, and getting notified of literally everything. As notifications rush by I may notice one or two relevant ones serendipitously, but I miss out on most of them.
2. Not watching the repository, so I only see notifications for stuff I'm explicitly mentioned in. So I miss out on pull requests I could proactively review.
What are some strategies I could adopt in order to keep abreast of interesting pull requests & issues on the repository, without being awash in notifications?
(One thought: maybe I could create smaller teams that people could add themselves to as interested, and ask that people tag the relevant teams. Or can teams be configured to automatically be tagged when certain parts of the code are touched?)
It looks like saved notification filters could be helpful. Unfortunately they don't support labels in filters, but filtering by person also works for me, because I work on a small team.
A Mastodon instance for programming language theorists and mathematicians. Or just anyone who wants to hang out.