On 12 October 2016 at 23:29, Andre Klapper aklapper@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.