-
Notifications
You must be signed in to change notification settings - Fork 167
Policies
** Draft, please add comments or extend, to discussed more Oct. 21th and following **
-
Branches behind Pull Request (PR) should be rebased to latest master before merging the PR. Reason is that this avoids a hard to read history with lots of parallel branches.
-
Pull Request should be merged by pressing the "Merge" button in the github UI. Reasons are because that way the branch is "grouped" by the resulting merge commit and, more important, the merging commit message has some pointer to the related PR and the discussion that might have happened on the PR.
Commits that are considered to not need review can be committed directly to master, without doing some PR dance. Again they should be done against the latest master, so the history is a single thread.
Usually the person who opened an issue should close it. (github automatically closing issues screws that slightly)