prune-remote-branches: add push option to prune remote branches
hg push --prune-remote-branches to a git remote will prune the remote's branches whose counterpart (topic) have been deleted.
hg push --prune-remote-branches to a git remote will prune the remote's branches whose counterpart (topic) have been deleted.