diff options
| author | coqbot-app[bot] | 2021-03-10 13:57:38 +0000 |
|---|---|---|
| committer | GitHub | 2021-03-10 13:57:38 +0000 |
| commit | cde4dceb93ba1f91d20f13a0fdea8f9731a6a626 (patch) | |
| tree | 92ff2503b55f731c3ef80c7f56150b98952aad68 /dev/doc | |
| parent | 317db327c21ac78bd921020118b19afaf1c02350 (diff) | |
| parent | 9955d2dfe778e41e447cb3ae71e708c7a3716f0d (diff) | |
Merge PR #13901: Fix list contributors
Reviewed-by: SkySkimmer
Diffstat (limited to 'dev/doc')
| -rw-r--r-- | dev/doc/release-process.md | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/dev/doc/release-process.md b/dev/doc/release-process.md index 57c325f698..1697a19668 100644 --- a/dev/doc/release-process.md +++ b/dev/doc/release-process.md @@ -114,6 +114,11 @@ list of contributors between Coq revisions. Typically used with `VX.X+alpha..vX.X` to check the contributors of version `VX.X`. + Note that this script relies on `.mailmap` to merge multiple + identities. If you notice anything incorrect while using it, use + the opportunity to fix the `.mailmap` file. Same thing if you want + to have the full name of a contributor shown instead of a pseudonym. + ## For each release (preview, final, patch-level) ## - [ ] Ensure that there exists a milestone for the following version. |