| Age | Commit message (Collapse) | Author |
|---|
|
|
|
I gave preference to the email address with the larger number of
commits.
To find duplicates, I used the script
```bash
for i in $(git shortlog -nse | sed s'/^\s*[0-9]*\s*//g' | grep -o '^[^<]*' | sed s'/\s*$//g' | sed s'/ /,/g'); do if [ $(git shortlog -nse | sed s'/ /,/g' | grep -c "$i") -gt 1 ]; then git shortlog -nse | grep "$(echo "$i" | sed s'/,/ /g')"; fi; done
```
|
|
|
|
|
|
I ran `git shortlog -nse | sed s'/^[ 0-9\t]*//g' | sort | less` and
manually inspected the result for duplicates.
Then I used
```bash
git shortlog -nse | sed s'/^[ 0-9\t]*//g' | sort | sed s'/<.*>//g' | uniq -c | grep -v '^ *1 '
```
to check that there were no remaining duplicates.
|
|
|
|
Of the three "anonymous" accounts, one ("coq") was used by multiple authors
(in particular Jacek Chrząszcz who developed the module system), while the
other two are each the committer of a single auto-generated commit so we rename
them to cvs2svn and serpyc-bot.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
The update process is as follows: run "git shortlog -s -e" and look for
duplicate or missing contributors.
|
|
|
|
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).
|
|
|
|
|
|
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.
|
|
|
|
|
|
|
|
In particular, this file allows to merge duplicated identities
of a same person. See man git shortlog for more details.
|
