Heads-up: master branch has been renamed to dev on 2nd Jan 2022

[McDutchie]

On the 1st of January I'll rename the master branch to dev as discussed in #386. Nothing else will change and dev will remain the default branch. But this will make it more obvious that this is where most active development and new feature testing happens, so users should expect some breakage every now and then. It will also save me some keystrokes when switching between branches. :)

I don't know if github will automagically redirect all operations to the new branch name, but if anything breaks as a result of the rename, your easiest fix will probably be to re-clone the repo.

[McDutchie]

OK, I've now done this, a day later than I planned.

The following commands will update your local git environment so you don't have to delete and re-clone the repo:

git branch -m master dev
git fetch -p origin
git branch -u origin/dev dev
git remote set-head origin -a

edit: or here's a one-liner version for convenient copy/pasting (I have a lot of local repos on test systems to update, maybe a few others of us do):

(set -x; git branch -m master dev && git fetch -p origin && git branch -u origin/dev dev && git remote set-head origin -a)