Re: git push tags

[Angelo Borsotti <angelo.borsotti@gmail.com>]

Hi Drew,

>
> Changing the tag in the local repository is a tag modification
> operation. Pushing that change to a remote repository DOES NOT execute
> "git tag...." in the remote. Plain and simple the two are different
> operations.
>

They are different for what concerns the implementation. They are not
necessarily so for what concerns their semantics, and the most
straightforward is to apply to the remote repository the changes done
on the local one -- the changes that can legally done on it -- and
changing a tag is not one allowed (unless forced).
Obviously, the semantics of git-push is different, and then needs to
be described clearly.
Note that some (probably most) of the operations that are disallowed
on the local repo are also disallowed by git-push, like, e.g. deleting
the current branch. But the user cannot tell what is disallowed and
what not if the man page does not state it.

> So here we come to the core argument. Is sounds to me like you want
> changes to remote tags to work differently from push updates to ALL
> other references. The required change, if I'm not mistaken, would be
> for tags to not permit fast-forward updates while all other references
> would be pushed normally. From my brief and un-enlightened look at the
> push code I can't see that being as easy as it sounds.
>

No, I was hoping that git-push refused to change tags at all, unless
forced (e.g. prefixing them with +), as it is on a local repository.

-Angelo