Git tricks
From xoa
If you want to do diffing from your local to a remote repo, you need to do a `git remote`.
git remote add main git://github.com/rakudo/rakudo.git git pull main
Then you can do
git diff main/master..origin/master
Git tagging
It's not enough to call git tag. You also have to do a git push --tags to push them back.