[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [Orekit Developers] Remove an accidental tag

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


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,

Best Regards,