On 17 October 2016 at 10:34, Tim Northover <t.p.northover at gmail.com> wrote: > I think this might be something to do with git not actually recording > empty directories. Could you have another look? Never mind, I've confirmed and committed a fix in r284401. Tim.