From 7b12da18b68731c3599d4e2ef841506a5df42bfa Mon Sep 17 00:00:00 2001
From: Alexandre Archambault <alexarchambault@users.noreply.github.com>
Date: Tue, 13 Feb 2018 14:56:25 +0100
Subject: [PATCH] Add note about merging PRs in DEVELOPMENT.md (#776)

---
 DEVELOPMENT.md | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/DEVELOPMENT.md b/DEVELOPMENT.md
index f82115d129..ab9f96f447 100644
--- a/DEVELOPMENT.md
+++ b/DEVELOPMENT.md
@@ -157,3 +157,11 @@ To build a distributable binary
 # Artifact will be placed under dist/
 java -jar dist/coursier-cli.jar fetch --help
 ```
+
+# Merging PRs on GitHub
+
+Use either "Create merge commit" or "Squash and merge".
+
+Use "Create merge commit" if the commit list is clean enough (each commit has a clear message, and doesn't break simple compilation and test tasks).
+
+Use "Squash and merge" in the other cases.