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

diff --cc Documentation/git-push.txt
Simple merge

diff --cc builtin/push.c
Simple merge