On 3/15/19 9:45 AM, Hartmut Goebel 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.
Eh, according to how I understand Git, this is wrong. When you rebase (against head), you move the commits of the branch on the end of the prior history, and thus do not require a *force* push. > 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 why what we do needs you to use an external repo. Maybe I am not understanding something. > >> 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? Not intentionally, but I don't see a way to avoid this without also allowing someone to do "damage" (deletion that cannot be easily undone). If there is a way to do this differently, please let us know and we'll deploy it. _______________________________________________ GNUnet-developers mailing list [email protected] https://lists.gnu.org/mailman/listinfo/gnunet-developers
