From 8646d5dbb59a5ee0b4bab2346315a9f97629a3c1 Mon Sep 17 00:00:00 2001 From: Ralf Jung <jung@mpi-sws.org> Date: Mon, 26 Jul 2021 11:53:03 +0000 Subject: [PATCH] Apply 2 suggestion(s) to 1 file(s) --- CONTRIBUTING.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 32b55a5bb..7225cdeab 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -36,10 +36,10 @@ 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 +We prefer small and self-contained merge requests that add a single feature 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 +(because it avoids blocking the whole merge request on a single discussion). ## How to update the std++ dependency -- GitLab