On 4/6/24 5:54 PM, Bruno Haible wrote: > It was caused by empty directories, which cannot be committed into git. > Thus in your checkout these directories are gone, while in my work > directory, they were still present.
Ah, that was my second guess. It works now, thanks. Collin