So my PR was merged - [https://github.com/github/linguist/pull/4866](https://github.com/github/linguist/pull/4866), but then reverted ([https://github.com/github/linguist/pull/4871](https://github.com/github/linguist/pull/4871)) because turns out some other language (Dafny) got a really similar colour before us - [https://github.com/github/linguist/pull/4841](https://github.com/github/linguist/pull/4841).
So can we please now have a discussion in this thread if we want the language colour change at all? I know a lot of people voted on that PR but it would be nice to hear more feedback :)
