> On 15. Mar 2019, at 09:45, Hartmut Goebel <h.goe...@crazy-compilers.com> > wrote: > > > Am 15.03.19 um 09:19 schrieb Christian Grothoff: >> Force pushes are never allowed, you must always rebase. > > Rebase also requiers a force push since the branch is not continuing the > prior history. > > I'm used to provide a series of patches for review, fix and clean up, > them merge or rebase. So for review I need to use an external repo, e.g. > at gitlab.digitalcourage.de. Not much of a problem for me, but this > hinders the reviewers workflow. >
I don't understand your problem. You can use another git repo as a mirror and work there if you want. It should just be another remote after all. You simply do: $ git checkout -b <mybranch> Do work $ git rebase master $ git checkout master $ git merge <mybranch> $ git push I do not see where you'd need to force push at any point. > >> AFAIK only admins can delete branches that have been pushed to the server. > > So after merging a branch I need to ask an admins to remove the old > branch? Is this a Arbeitsbeschaffungsmaßname? Hopefully we will have a gitlab setup at some point that allows us to deal with this using user namespaces and pull requests. Anyway, deleting branches is not really necessary, but I agree that it will clutter the main server remote unless we have such a setup. > > -- > Regards > Hartmut Goebel > > | Hartmut Goebel | h.goe...@crazy-compilers.com | > | www.crazy-compilers.com | compilers which you thought are impossible | > > > _______________________________________________ > GNUnet-developers mailing list > GNUnet-developers@gnu.org > https://lists.gnu.org/mailman/listinfo/gnunet-developers
signature.asc
Description: Message signed with OpenPGP
_______________________________________________ GNUnet-developers mailing list GNUnet-developers@gnu.org https://lists.gnu.org/mailman/listinfo/gnunet-developers
