+ [2020-06-21T17:26:52Z] sm[m] well, not quite.
+ [2020-06-21T17:28:08Z] sm[m] I deleted it with git push origin :refs/heads/1.18 (since git push -d origin :refs/heads/1.18 fails, "matches more than one"). And I deleted the tag locally, which was recreating it on push.
+ [2020-06-21T17:29:27Z] sm[m] Now unfortunately I found another bogus tag, this time named "refs/heads/master". This one I can't delete remotely by either of those push commands
+ [2020-06-21T17:31:22Z] sm[m] I wonder what's another way to delete this tag on github
+ [2020-06-21T17:32:30Z] sm[m] haha, found it: git push origin :refs/tags/refs/heads/master

message no. 182612

Posted by sm[m] in #github at 2020-06-21T01:37:21Z

g'day all. I made a github release with a signed tag named 1.18. I forgot I use that naming for release branches, so I'd like to rename the tag to r1.18. Would you know if I can do this, without messing up the github release ?
+ [2020-06-22T19:27:42Z] kiorky I have problem resolving github.com (DNS) for the last hour, 40% of (A) DNS queries are failing.
+ [2020-06-22T19:27:59Z] kiorky reproducible with dig github.com @8.8.8.8 +short
+ [2020-06-22T19:35:39Z] dka is github down?
+ [2020-06-22T19:41:33Z] kiorky dka: seems they have some DNS issues, you are not alone to have problems.