I did try a force push *immediately* but since the branch was locked it was rejected. I took that as a sign to revert. I generally avoid force pushing unless the repo is used by me or only a very small number of people.

On Jun 3, 2024, at 9:14 AM, pd-dev-request@lists.iem.at wrote:

Message: 2
Date: Sun, 2 Jun 2024 23:40:21 +0200
From: IOhannes m zm?lnig <zmoelnig@iem.at>
To: pd-dev@lists.iem.at
Subject: Re: [PD-dev] Whoops, pushed to master
Message-ID: <35c749e7-60b5-4228-8492-67c0358aca06@iem.at>
Content-Type: text/plain; charset="utf-8"; Format="flowed"

On 6/2/24 21:37, Christof Ressi wrote:
Hi Dan,

On 02.06.2024 14:40, Dan Wilcox wrote:
Howdy all,

sorry, I accidentally pushed a couple of commits to the master branch. 
I reverted them after I realized. I suppose there is no clean way to 
handle this otherwise.

No worries, this has happened to me as well :) In the future, this is 
what you can do:

1. GitHub: in the repo settings (temporarily) enable force pushing to 
master

2. git reset <previous_master_head>

3. git push -f

4. GitHub: disable force pushing to master again


this is what i would do (and have done!) in the same situation as well.

i was going to suggest that i could do that for dan, but miller has 
already pushed on top your reverting commits, so I guess somebody will 
have to live with eternal shame (or just keep contributing) :-)

--------
Dan Wilcox
danomatika.com
robotcowboy.com