Hi, Somebody just pointed me out that the commit dd0d19d04b51fee0f173f3334874fb53a2112461 contents isn't part of master anymore, but there's no visible commit (i.e. in git log -p) that removes its contents. Maybe some git merge went wrong? Aleix