From ab8d7e5ddcbec8307ed6fd5871e1a7349e8fe93a Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 26 Jul 2021 12:12:29 +0200
Subject: [PATCH] Expand `CONTRIBUTING.md` with information that we prefer
 small merge requests.

---
 CONTRIBUTING.md | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
index 3295c1e42..32b55a5bb 100644
--- a/CONTRIBUTING.md
+++ b/CONTRIBUTING.md
@@ -36,6 +36,12 @@ a feature branch instead.
 [jung]: https://gitlab.mpi-sws.org/jung
 [iris]: https://gitlab.mpi-sws.org/iris/iris
 
+We prefer small and self-contained merge requests that add a single features
+over merge requests that add arbitrary collections of lemmas. Small merge
+requests are easier to review, and will typically be merged more quickly
+(because it avoids that the whole merge request will be blocked on a single
+discussion).
+
 ## How to update the std++ dependency
 
 * Do the change in std++, push it.
-- 
GitLab