Merge branch 'jk/pull-to-integrate'
commit5b307e95e880b95eafd36e93251c6638c222dcf4
authorJunio C Hamano <gitster@pobox.com>
Fri, 12 Jul 2013 19:04:06 +0000 (12 12:04 -0700)
committerJunio C Hamano <gitster@pobox.com>
Fri, 12 Jul 2013 19:04:06 +0000 (12 12:04 -0700)
tree0d511facc0fe5969d5b923dde557349997be5a19
parente70aee5c86c508af4a92bd02b688b4aa39c58180
parent153d7265ef1277c1c9971780ad035a530e305f78
Merge branch 'jk/pull-to-integrate'

* jk/pull-to-integrate:
  pull: change the description to "integrate" changes
  push: avoid suggesting "merging" remote changes
builtin/push.c
git-pull.sh