Jeff King <p...@peff.net> wrote:
> On Tue, Apr 11, 2017 at 02:37:27PM +0200, Stefan Haller wrote:
>
> > Are you talking about the case where the user doesn't say git pull, but
> > instead says "git fetch && git merge --ff @{u}"? Just so that I
> > understand the concern.
>
> Yes, that (which is the main way that I merge changes).
OK; in my proposal I already mentioned that a few other commands besides
push and pull may have to update the lease; examples I mentioned were
git rebase @{u}
git reset @{u}
and you add "git merge --ff @{u}" to that list now. There might be
others that we can add to make the feature work better. (But this could
happen incrementally later, as we learn about more use cases.)
> But also what happens with:
>
> git merge origin/other-branch
> git rebase origin/master
>
> I think we only care when origin/master has independently merged
> other-branch, too. And even though we have taken its commits into
> account, we would fail (because "both sides did the same thing" is
> really out of scope for the concept of a lease). So that's OK.
I think there's nothing special to consider here; "git rebase
origin/master" updates the lease (to origin/master), period. It doesn't
matter whether origin/other-branch was merged before, or whether or not
it was independently merged to origin/master too, or whether our local
branch has cherry-picked all the commits of other-branch instead of
merging it, or whatever. In all these cases, the local branch is "up to
date" with origin/master after the rebase, so it's ok to update the
lease at that point.
--
Stefan Haller
Berlin, Germany
http://www.haller-berlin.de/
