The git commands work great, but it leaves a `remotes/origin/HEAD` pointing to the (now-deleted) 'remotes/origin/master'. This triggers a warning if you try to do some housecleaning of the dangling `origin/master` using the `git remote prune origin` command. You need to run 2 more commands if you want a pristine local repo that's equivalent to doing a fresh 'git clone`:
$ git remote set-head origin -a # automatically determine default, which will be `origin/main`
$ git remote prune origin # remove `origin/master` from the local repo
Personally, I'm not convinced that GitHub's push for this rename will make a meaningful difference for the underlying social problem, but this is not too much work either. Though I had to do it for 5 laptops, and this broke 3 of my continuous integration scripts... but nothing major.
Brian