aboutsummaryrefslogtreecommitdiffhomepage
path: root/.mailmap
Commit message (Collapse)AuthorAge
* Update the .mailmap file.Gravatar Guillaume Melquiond2017-04-08
|
* Deduplicate some names in .mailmapGravatar Jason Gross2016-07-06
|
* Add mailmap entry.Gravatar Guillaume Melquiond2016-07-05
|
* Update the .mailmap file.Gravatar Guillaume Melquiond2015-10-05
| | | | | The update process is as follows: run "git shortlog -s -e" and look for duplicate or missing contributors.
* Add t-jagro to .mailmapGravatar Jason Gross2014-08-26
|
* "allows to", like "allowing to", is improperGravatar Jason Gross2014-08-25
| | | | | | | | | | | It's possible that I should have removed more "allows", as many instances of "foo allows to bar" could have been replaced by "foo bars" (e.g., "[Qed] allows to check and save a complete proof term" could be "[Qed] checks and saves a complete proof term"), but not always (e.g., "the optional argument allows to ignore universe polymorphism" should not be "the optional argument ignores universe polymorphism" but "the optional argument allows the caller to instruct Coq to ignore universe polymorphism" or something similar).
* More .mailmap update.Gravatar Arnaud Spiwack2014-08-07
|
* Add some more entries to .mailmapGravatar Arnaud Spiwack2014-08-07
|
* Update .mailmap with recent contributors.Gravatar Arnaud Spiwack2014-01-17
| | | | | I should have updated everyone who committed since the migration to git (giving me a canonical email). I've search git shortlog -s to ensure the best IĀ could that there are no duplicate. I discovered that email addresses from the mailmap are uncapitalised whereas the unmodified addresses are not, creating two different authors for no reason. So, I've added some record to normalise the canonical email addresses when needed.
* Use my real email address in .mailmapGravatar Enrico Tassi2013-11-27
|
* updated .mailmapGravatar Pierre Letouzey2013-11-21
|
* update .mailmap with my email now that I've used it in a commitGravatar Pierre Letouzey2013-11-19
|
* A .mailmap file for a nice git-shorlog displayGravatar Pierre Letouzey2013-11-19
In particular, this file allows to merge duplicated identities of a same person. See man git shortlog for more details.