GitHub: add public developer team with team's mention @dealii

[Denis Davydov]

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.

[Matthias Maier]

That sounds like a nice idea.

I simply went ahead and renamed the developer team to "dealii" and made
it public.

Best,
Matthias

[Denis Davydov]

Cool! Thanks for the prompt action!

> 6 дек. 2016 г., в 20:34, Matthias Maier <tam...@43-1.org> написал(а):

> --
> You received this message because you are subscribed to a topic in the Google Groups "deal.II developers" group.
> To unsubscribe from this topic, visit https://groups.google.com/d/topic/dealii-developers/EkQxkQrM_Vc/unsubscribe.
> To unsubscribe from this group and all its topics, send an email to dealii-develop...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.