Merge branch 'jc/push-delete-nothing'

"git push $there --delete ''" should have been diagnosed as an error, but instead turned into a matching push, which has been corrected. * jc/push-delete-nothing: push: do not turn --delete '' into a matching push