on master help sign in
update pr merge checklist
commit879d159ff2469d92d6baacb826112fc45a1ac2ce authorHarendra Kumar <harendra.kumar@gmail.com> dateSun 8 Dec 2019, 09:08 (7 years ago) parent42f1091
1 file changed+8−4
MAINTAINING.md+8−4
MAINTAINING.md+8−4
@@ -5,11 +5,15 @@
55* All the CI tests pass
66* New tests are added where applicable
77* Benchmarks are added where applicable
8−* hlint
98* Run benchmarks locally if you suspect any regressions
10−* If the PR is by someone other than you yourself then merge with a merge
11− commit, otherwise merge by rebasing on master without a separate merge
12− commit.
9+* Documentation is added for any new combinators
10+* Changelog entry is added for exposed combinators.
11+* Optionally, look at hlint output if anything in that is worth fixing.
12+* Merge the PR by rebasing. Note that github always creates new commits when
13+ merged with rebase, it records the committer as well as the author in the
14+ commit. This makes the local branch diverge from master. You can rebase and
15+ merge the commit manually in your local git tree and push the resulting
16+ master branch to avoid new commits and divergence from the original tree.
1317
1418## Release Checklist
1519