News for hackers. Stuff that matters.
Re:Incident with Issues and Pull Requests by capableweb on Thursday May 11, 2023 @09:51AM (#35902087)
How??? You do the merge, which either creates a new commit for the change, or appends the commits to your existing tree. Then you push that to the remote. If the push fails, you can just push again, it's not lost. And if the merge failed, you didn't have any merge commit to begin with.
Re:Incident with Issues and Pull Requests by misnome on Thursday May 11, 2023 @10:07AM (#35902297)
There used to be a pretty consistent bug that if an on-site PR merge failed but you clicked "Retry", that it just did a basic non-squash full-merge discarding all your commit message work, often requiring a revert to tidy things up. It could be similar to that.
Re:Incident with Issues and Pull Requests by edgyquant on Thursday May 11, 2023 @10:11AM (#35902367)
May have been using the GitHub interface
Re:Incident with Issues and Pull Requests by snapcaster on Thursday May 11, 2023 @11:17AM (#35903404)
You can do a lot of operations on the github web UI nowadays. Could have been that