On 12 October 2016 at 23:29, Andre Klapper <aklapper(a)wikimedia.org> wrote:
https://gerrit.wikimedia.org/r/#/c/211034/
Move up devunt's name to Developers
/CREDITS
I think we have combined both those lists into one and just have
CREDITs now sorted alphabetically.