It is a common mistake to leave an unsed `origin` branch behind
if a shared public repository was created by first cloning from
somewhere else. Subsequent `git push` into it with the default
"push all the matching ref" would push the `origin` branch from
the developer repository uselessly.