Thank you so much, Panos. Yes, exactly that's the intention.
On Sun, Jan 10, 2021 at 10:49 AM Panos Garefalakis <[email protected]> wrote: > Hey Dongjoon, > > Definitely agree with the suggestion +1. > I guess one could still merge locally and push (not sure if there is > anything we can do there) but we would avoid tricky situations caused by > merging using the GitHub UI. > > Cheers, > Panagiotis > > On Fri, Jan 8, 2021 at 2:10 AM Dongjoon Hyun <[email protected]> > wrote: > > > Hi, All. > > > > GitHub provides three merge options like the following. > > I'd like to propose to disable the `Create a merge commit` option (the > > first one) explicitly to keep the same behavior with our merge practice > > before GitHub Era. > > It will remove accidental `merging and force-push` situations. What do > you > > think? > > > > [image: Screen Shot 2021-01-07 at 4.05.41 PM.png] > > > > Bests, > > Dongjoon. > > >
