[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[Orekit Developers] Remove an accidental tag
- To: <orekit-developers@orekit.org>
- Subject: [Orekit Developers] Remove an accidental tag
- From: Evan Ward <evan.ward@nrl.navy.mil>
- Date: Mon, 14 Nov 2016 14:53:35 -0500
- User-agent: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101 Thunderbird/45.4.0
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.
Best Regards,
Evan