[Agda] Wrong number of commits on GitHub
Andrés Sicard-Ramírez
asr at eafit.edu.co
Thu Jun 19 23:47:23 CEST 2014
Hi,
As possibly some of you know, the number of commits associated to some Agda
or the standard library developers/contributors shown in
https://github.com/agda/agda/graphs/contributors
and
https://github.com/agda/agda-stdlib/graphs/contributors
is wrong.
You can fix it by following the account linking instructions in
https://help.github.com/articles/i-don-t-see-myself-in-the-repository-contributors-graph
You can see your used email address in the files
Agda: https://github.com/agda/agda/blob/master/.mailmap
Standard library: https://github.com/agda/agda-stdlib/blob/master/.mailmap
and by running the command
$ git shortlog -nse
(If you find something wrong in the .mailmap files, make a pull request
please)
Best,
--
Andrés
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20140619/81096b9e/attachment.html
More information about the Agda
mailing list