Github mirror out of sync

[Julien Massiera]

Hi,

 

I am not sure it has been reported but the Github mirror seems out of sync
with the SVN repo since June

 

Julien