tree 9a8bb3c516eb72c8a5141dd3c162e3dc2d34d186
parent cadae717d557840d3566b7c0fc2003046e08c88f
parent 20e416409fc2bc260faf65a0fc74927ed0d3ca12
author Junio C Hamano <gitster@pobox.com> 1614300212 -0800
committer Junio C Hamano <gitster@pobox.com> 1614300213 -0800

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