From dbfee23682d5278f7f42f7e1e9657fd19ca2c93b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 16 Aug 2017 14:22:32 -0700 Subject: [PATCH] chore(.github/CONTRIBUTING.md): update PR submission guidelines. --- .github/CONTRIBUTING.md | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/.github/CONTRIBUTING.md b/.github/CONTRIBUTING.md index 37e4ddad17..84edcde8de 100644 --- a/.github/CONTRIBUTING.md +++ b/.github/CONTRIBUTING.md @@ -22,8 +22,13 @@ for you (the contributors) and us (the maintainers). # Opening Pull Requests +The core developers have to maintain Lean. Thus, they need to read all PRs, and make sure they can maintain them. +So, here are some guidelines for submitting PRs: +- Small bug fixes are always welcome. +- Before implementing a major feature or refactoring the code, please ask whether the change is welcome or not. + The worst kind of PR is the "unwanted one". That is, we don’t want it, but we have to explain why we will not merge it. +- Ensure all test suite works before submitting a PR. - Ensure your Pull Request meets the coding and commit conventions documented above. - Ensure your Pull Request contains tests for the behavior, for both features or bug fixes. - - +- If you are not proficient in C++, do not submit PRs with C++ code.