Hi, >> > 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.
Yeah, sorry. I didn’t realize wip-r was worked on by any one other than simon and myself. The commits are still there, they just don’t have a named pointer (= branch) to them any longer: https://git.savannah.gnu.org/cgit/guix.git/log/?id=8ed6a08a998d4abd58eb67c85699f38f87f76d05 If that’s the last commit (or if you have another one that was pushed) I can simply reset the branch pointer to it and then stay out of it :) > >> 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. Deleting the branch is “git push -d origin wip-r”. >> 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. Same. I prefer having a branch so ci.guix.gnu.org can build things and we can keep an eye on the fall-out (if any). Sorry again for making this harder than it should be! -- Ricardo