Quick changes in repository name

This is just a quick memo to future self on what should be done locally, if I rename some GitHub repo:

git pull
git push
git prune
git remote prune origin
git status

Or even faster:

git pull && git push && git prune && git remote prune origin && git status

I am changing a lot of my repos’ names to figure out some static scheme. This is a “toolset” for that process.