I think it would be better if deal.II's GitHub account had developer team public and the possibility to address all developers via team's mention of @dealii or alike.
See https://help.github.com/articles/setting-up-teams/ for details. p.s. I would say the usage case is to ping on PRs which are ready, but need at least one more pair of eyes to review. Cheers, Denis. -- You received this message because you are subscribed to the Google Groups "deal.II developers" group. To unsubscribe from this group and stop receiving emails from it, send an email to dealii-developers+unsubscr...@googlegroups.com. For more options, visit https://groups.google.com/d/optout.
