Hi Roel, On Thu, 19 Nov 2020 at 20:03, Roel Janssen <r...@gnu.org> wrote:
> > http://logs.guix.gnu.org/guix/2020-11-19.log#182349 > Right, so I shouldn't have pushed to "wip-r" in the first place. Well, I think it is a lack of synchronisation between all of 3; especially with this work around via external GitHub upstream. > Perhaps I should do it "the old way" and base my patches on the master > branch and send the gazillion patches to the mailing list. :) What Ricardo did previously (my rewrite of history on Nov. 10 on GitHub, and then pushed by Ricardo to Savannah today), quoting their word: "delete origin/wip-r, reset my local copy to zimoun/wip-r, rebased on top of origin/master, and pushed origin/wip-r". Maybe you could do the same. Or if you have the super power to do that: you can delete the branch and re-push. > Then we can discuss each line of the commit messages separately before > pushing to the master branch. Well, I do not know what Ricardo thinks, but personally I would prefer first a wip-r branch then merge. It will avoid avoid annoyance of possible broken packages, I mean we could detect them. All the best, simon