On Tue, Dec 6, 2016, at 13:07 CST, Denis Davydov <davyd...@gmail.com> wrote:
> 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. That sounds like a nice idea. I simply went ahead and renamed the developer team to "dealii" and made it public. Best, Matthias -- 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.
