diff options
| author | Jason Gross | 2019-04-10 22:58:48 -0400 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-04-29 20:29:58 +0200 |
| commit | 8e97ed087e8e60dd5d05d7a3381083af92a8021b (patch) | |
| tree | 3a052ca4c0e4ee8e3d16ecf62e9dd568d05845f3 /doc/plugin_tutorial/tuto2/_CoqProject | |
| parent | 75dc5da6ceefb30bd741971f303c95d3af1622de (diff) | |
Add some entries to .mailmap
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.
Diffstat (limited to 'doc/plugin_tutorial/tuto2/_CoqProject')
0 files changed, 0 insertions, 0 deletions