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. -- The deal.II project is located at http://www.dealii.org/ For mailing list/forum options, see https://groups.google.com/d/forum/dealii?hl=en --- You received this message because you are subscribed to the Google Groups "deal.II User Group" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. For more options, visit https://groups.google.com/d/optout.
