Merge branch 'ps/push-delete-option'

"branch --delete" has "branch -d" but "push --delete" does not. * ps/push-delete-option: push: add '-d' as shorthand for '--delete' push: add '--delete' flag to synopsis

Junio C Hamano committed Jan 12, 2016 at 15:16 UTC 7b9d1b9556b31fe5f661caa1e82856ca876f2a08

No changes.