Git: remove a local branch after it was deleted on the remote repository

in Geek Inside

That’s useful after closing a pull request and removing a branch on GitHub.

git fetch -p