Can github activity (new PRs, comments) be forwarded to dev@ ?

[Yann Ylavic]

That'd help being more reactive there, avoid having multiple places to
follow, avoid tenchnical discussions taking place outside our mailing
lists...

Probably more a question for infra, but what does the team think?