Join GitHub today
GitHub is home to over 50 million developers working together to host and review code, manage projects, and build software together.Sign up
monitor: 0.7.1 -> 0.7.2 #86983
Motivation for this change
(As a side note, I changed my GitHub username without thinking about the side effect it would have on the nixpkgs I maintain. Should I make a pull request to update it, or leave it as it is now ? As I've understood, people can always find me through my GitHub id anyway)
It would be great if that attribute was the same as your github username.