+ [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. 182615

Posted by famubu in #github at 2020-06-21T10:23:17Z

I have a branch which was merged to master. After while I noticed a bug in it and fixed it. Should I commit to the same branch (with which the original PR was made) or should I make a new PR?
+ [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.