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.