Re: [Orekit Developers] Remove an accidental tag

[MAISONOBE Luc <luc.maisonobe@c-s.fr>]

Evan Ward <evan.ward@nrl.navy.mil> a écrit :

> Hi,
>
> At some point I accidentally pushed the tag "orekit-8.0-evan1". I  
> was trying to work around #252 and didn't intend to push it yet.  
> I've tried deleting it myself with these commands:
>
> git tag -d orekit-8.0-evan1
> git push origin :refs/tags/orekit-8.0-evan1
>
> but I get:
>
>  ! [remote rejected] orekit-8.0-evan1 (hook declined)
>
> Is there a way to delete a tag? My only concern is that it doesn't  
> match the project's tagging convention.

I'll see if I can do it directly on the server. Currently, I cannot
ssh to it, I'll see tomorrow.

Anyway, it is not really a problem, the tag can remain there.

best regard,
Luc

> Best Regards,
> Evan