From 72180192bd426e1c9e5ac5fe98bc4ea22e1c7a6f Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Fri, 9 Aug 2019 11:47:16 +0200
Subject: Recommend assigning an issue before fixing a bug.

Contributors with write-access can now assign people who commented an issue:
https://github.blog/changelog/2019-06-25-assign-issues-to-issue-commenters/
---
 CONTRIBUTING.md | 26 ++++++++++++++++++++++----
 1 file changed, 22 insertions(+), 4 deletions(-)

(limited to 'CONTRIBUTING.md')

diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
index 529a912bb6..bf07e37ef4 100644
--- a/CONTRIBUTING.md
+++ b/CONTRIBUTING.md
@@ -616,8 +616,26 @@ documentation][coqdoc-documentation] to learn more.
 
 ### Fixing bugs and performing small changes ###
 
-Just open a PR with your fix.  If it is not yet completed, do not
-hesitate to open a [*draft PR*][GitHub-draft-PR] to get early
+Before fixing a bug, it is best to check that it was reported before:
+
+- If it was already reported and you intend to fix it, self-assign the
+  issue (if you have the permission), or leave a comment marking your
+  intention to work on it (and a contributor with write-access may
+  then assign the issue to you).
+
+- If the issue already has an assignee, you should check with them if
+  they still intend to work on it.  If the assignment is several
+  weeks, months, or even years (!) old, there are good chances that it
+  does not reflect their current priorities.
+
+- If the bug has not been reported before, it can be a good idea to
+  open an issue about it, while stating that you are preparing a fix.
+  The issue can be the place to discuss about the bug itself while the
+  PR will be the place to discuss your proposed fix.
+
+In any case, feel free to just ignore the recommendation above, and
+jump ahead and open a PR with your fix.  If it is not yet complete, do
+not hesitate to open a [*draft PR*][GitHub-draft-PR] to get early
 feedback, and talk to developers on [Gitter][].
 
 It is generally a good idea to add a regression test to the
@@ -638,12 +656,12 @@ merged.
 
 So it is recommended that before spending a lot of time coding, you
 seek feedback from maintainers to see if your change would be
-supported, and if they have recommendation about its implementation.
+supported, and if they have recommendations about its implementation.
 You can do this informally by opening an issue, or more formally by
 producing a design document as a [Coq Enhancement Proposal][CEP].
 
 Another recommendation is that you do not put several unrelated
-changes (even if you produced them together) in the same PR.  In
+changes in the same PR (even if you produced them together).  In
 particular, make sure you split bug fixes into separate PRs when this
 is possible.  More generally, smaller-sized PRs, or PRs changing less
 components, are more likely to be reviewed and merged promptly.
-- 
cgit v1.2.3