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

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