Merge branch 'jk/push-default-doc'
authorJunio C Hamano <gitster@pobox.com>
Wed, 12 Feb 2020 20:41:36 +0000 (12:41 -0800)
committerJunio C Hamano <gitster@pobox.com>
Wed, 12 Feb 2020 20:41:36 +0000 (12:41 -0800)
commit4cf7f48891d36d9ec3783119ddc1177fa9f0581e
tree420dcaa655df8548f51ae8cc9fd64729ea448109
parentb7833910180d7d762ad0bb0f59cb02ba9ef86710
parent8b2a1928f08a0c795de1a84aa329bc85dcdb3949
Merge branch 'jk/push-default-doc'

Doc update.

* jk/push-default-doc:
  doc: drop "explicitly given" from push.default description