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, [email protected] wrote: > > Message: 2 > Date: Sun, 2 Jun 2024 23:40:21 +0200 > From: IOhannes m zm?lnig <[email protected] <mailto:[email protected]>> > To: [email protected] <mailto:[email protected]> > Subject: Re: [PD-dev] Whoops, pushed to master > Message-ID: <[email protected] > <mailto:[email protected]>> > 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 <http://danomatika.com/> robotcowboy.com <http://robotcowboy.com/>
_______________________________________________ Pd-dev mailing list [email protected] https://lists.puredata.info/listinfo/pd-dev
