Ask HN: Have you ever changed your GitHub username?

I'm considering doing this, but as it says here[0], it's not that clean of a transition:

- any comments that @mentioned you will still use the old username

- someone else can come and take your old username, although it sounds like there are ways to get them to retire it, e.g. cloning one of your public repos 100 times in the week before you rename it. Has anyone had success with this?

[0]: https://docs.github.com/en/account-and-profile/setting-up-and-managing-your-personal-account-on-github/managing-personal-account-settings/changing-your-github-username