On Thu, 2018-10-11 at 14:59 -0400, Bruce Ashfield wrote: > merged. > > I had git rm'd it locally, but forgot to commit and push the change > :D Thanks, its the kind of little bug which was irritating me more than it should :) Cheers, Richard