I did a rebase (which turned into a no-op as expected) and a force push. So now master and site both point to dc69a4515.
> On Jul 20, 2018, at 3:53 PM, Michael Mior <mm...@apache.org> wrote: > > I actually didn't make any changes since you sent your message (site > still contains a merge commit). I'm happy with whatever direction > others want to take. > > -- > Michael Mior > mm...@apache.org > Le ven. 20 juil. 2018 à 18:32, Julian Hyde <jh...@apache.org> a écrit : >> >> Thanks for the tip, Andrew. I’ll give that a try. I may yet come to love >> merge commits! >> >> I saw that Michael reset “site”. Thank you - I think it was the right choice >> in this case. >> >> >>> On Jul 20, 2018, at 11:54 AM, Andrew Pilloud <apill...@google.com> wrote: >>> >>> git log --simplify-merges is probably what you are looking for. Merges are >>> a important tool in busy public repos. >>> >>> On Fri, Jul 20, 2018 at 2:49 PM Michael Mior <mm...@apache.org >>> <mailto:mm...@apache.org>> wrote: >>> I'm fine with that. I can always reset and do a force push. >>> >>> -- >>> Michael Mior >>> mm...@apache.org <mailto:mm...@apache.org> >>> >>> Le ven. 20 juil. 2018 à 14:38, Julian Hyde <jh...@apache.org >>> <mailto:jh...@apache.org>> a écrit : >>>> >>>> Michael, >>>> >>>> I saw you merged the site branch. I had been thinking of instead doing a >>>> rebase. >>>> >>>> I did a test rebase a few days ago and was pleased to see that it went >>>> smoothly — meaning that every commit in “site” had also been made to >>>> “master” — and it ended up pointing to the same commit as master. >>>> >>>> In my opinion, merge commits are fine in personal repos but they are not >>>> great in public repos because they usually obfuscate history. (Maybe I >>>> just haven’t found the right tools to view them.) In this case, I think >>>> ‘git checkout site; git rebase origin/master; git push origin site’ would >>>> have been better. >>>> >>>> Julian >>>> >>> >>> On Fri, Jul 20, 2018 at 2:49 PM Michael Mior <mm...@apache.org >>> <mailto:mm...@apache.org>> wrote: >>> I'm fine with that. I can always reset and do a force push. >>> >>> -- >>> Michael Mior >>> mm...@apache.org <mailto:mm...@apache.org> >>> >>> Le ven. 20 juil. 2018 à 14:38, Julian Hyde <jh...@apache.org >>> <mailto:jh...@apache.org>> a écrit : >>>> >>>> Michael, >>>> >>>> I saw you merged the site branch. I had been thinking of instead doing a >>>> rebase. >>>> >>>> I did a test rebase a few days ago and was pleased to see that it went >>>> smoothly — meaning that every commit in “site” had also been made to >>>> “master” — and it ended up pointing to the same commit as master. >>>> >>>> In my opinion, merge commits are fine in personal repos but they are not >>>> great in public repos because they usually obfuscate history. (Maybe I >>>> just haven’t found the right tools to view them.) In this case, I think >>>> ‘git checkout site; git rebase origin/master; git push origin site’ would >>>> have been better. >>>> >>>> Julian >>>> >>
