Re: [Orekit Developers] Remove an accidental tag

[Luc Maisonobe <Luc.Maisonobe@c-s.fr>]

Le 14/11/2016 à 22:27, MAISONOBE Luc a écrit :
> 
> 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.

Done.

best regards,
Luc

> 
> Anyway, it is not really a problem, the tag can remain there.
> 
> best regard,
> Luc
> 
>>
>> Best Regards,
>> Evan