On Thu, 16 Jul 2015, Brendan Scott wrote: > > Why don't you add a directory on the git repo for docs? > Good suggestion, I'd prefer to put it in a separate git repo, though, because our current git repo is already top-heavy! Boudewijn