2018-12-15 UTC
# 
jeremycherfas I also realised that I was getting myself in a right old mess with git by having an origin/dev branch. I really don't need it, unless I am moving from desktop to laptop, because I do it all myself and so only need to merge in master locally. That has simplified my life a bit.