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. >
