Administrator Guidelines

These instructions are only relevant to those who have been granted push rights on the upstream repository (those who are in the spring-integration-admin group). Contributors, even admin group members when contributing code, should consult the [Contributor Guidelines](Contributor Guidelines).

Merging Pull Requests

The following steps indicate a typical merge of a Pull Request once its review is complete and it has been approved by at least one team member (other than the original contributor). Note that the button on github can also merge a PR (our comment below emulates the comment it would generate), but while that will only be enabled if the PR can merge cleanly, it will not check if the PR is up-to-date with respect to upstream/master. In order to maintain a clean linear history (with only merge commits being non-linear), the following steps include a rebase (and optionally, an interactive squashing rebase as well).

// sync up
git fetch --all

// make sure your local master is up to date
git checkout master
git merge upstream/master

// grab the branch for the PR
git checkout --track johndoe/INT-123 

// make sure that branch is up-to-date
git rebase master

// get a quick view of the number of commits past upstream/master
git log --oneline

// At this point, you might even do some basic polishing, but typically
// that should be handled by the original committer via PR feedback.
// - Check copyright dates
// - Include a check for whitespace violations and fix or bounce back to contributor.
git log -p --check

// IF you want to squash (no historical value) do an interactive rebase;
// 3 in this case (HEAD~3) being an example number of commits to squash.
git rebase -i HEAD~3

// Do a full build
./gradlew build

// go back to the local master
git checkout master

// merge the local tracking branch into master with a comment having this format (and no fast-forward)
git merge -m "Merge pull request #99 from johndoe/INT-123" --log --no-ff INT-123

// polish the results of the previous --log if necessary
git commit --amend

// push to your own fork's master
git push origin master

// push to THE upstream master
git push upstream master

After the branch has been merged, if that branch did require rebasing master, then it will not be automatically closed within github. If that's the case, manually close the PR in github, optionally including a comment. GitHub will close the PR if no rebase was required, but you should check the PR list anyway.