On Thu, 19 Nov 2020 at 16:57, Roel Janssen <r...@gnu.org> wrote: > My bad, I jumped to a conclusion too quickly. :)
No worries. :-) > So, *something* removed my commits to the wip-r branch. Is it some kind > of automation that syncs the Github and the Savannah branches? Which upstream? I have no access on Savannah. And I think you could should there. My wip-r branch on my personal GitHub account, no automation. Ricardo did couple of days ago: fetch my branch and push it to Savannah. Then they reported a tiny mistake that I corrected on my branch, by rewriting the history since it is WIP. It was before you have started to work on, I guess. To be concrete, the last commit on my branch is 9 days ago. And the last commit on Savannah wip-r is 30th Otc. > The good news is that in my local checkout I've fixed the build problem > with r-rhdf5lib, so I should be able to build the remaining packages > this evening. Really cool! Thank you. > I am hesitant to push it to the "wip-r" branch, because it seems > pointless. :) So where can I push my updates to? Please push your changes to wip-r on Savannah, rewriting the history is fine with me. Then Cuirass will rebuild everything, check. Then we can merge to master. All the best, simon