aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
authorThéo Zimmermann2021-03-05 15:03:59 +0100
committerThéo Zimmermann2021-03-05 15:12:08 +0100
commitafa4882102d627ce5be6821f591f3bf42fe74324 (patch)
treeae735d54eece02be7898d8111b328e0648b18d08 /dev
parentef148d7d14ce2f6782d47186bc944851893e39eb (diff)
Document the relation of the list-contributors.sh script to .mailmap.
Diffstat (limited to 'dev')
-rw-r--r--dev/doc/release-process.md5
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.