Hi, All. This setting is applied.
https://issues.apache.org/jira/browse/INFRA-21289 https://issues.apache.org/jira/browse/ORC-725 Thanks, Dongjoon. On Sun, Jan 10, 2021 at 4:15 PM Dongjoon Hyun <[email protected]> wrote: > 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. >> > >> >
