Github PR merging strategy

[oldk1331]

Hi Waldek,

Which is your preferred way of merging PR?

Merge directly or rebase?

I prefer rebase because I like linear history.

- Qian

[Ralf Hemmecke]

Hi Qian,

I definitely prefer rebase for simple commit. I do not like these extra
merge commits.

In fact, FriCAS only has one non-linearity in the commit DAG. At that
time I asked Waldek whether I should turn the merge into a rebase, but
it was already public so I left it. Otherwise, at that time Waldek
preferred to keep the commit DAG linear.

Ralf

[Waldek Hebisch]

On Thu, Jan 21, 2021 at 04:22:12PM +0100, Ralf Hemmecke wrote:
> Hi Qian,
>
> I definitely prefer rebase for simple commit. I do not like these extra
> merge commits.
>
> In fact, FriCAS only has one non-linearity in the commit DAG. At that
> time I asked Waldek whether I should turn the merge into a rebase, but
> it was already public so I left it. Otherwise, at that time Waldek
> preferred to keep the commit DAG linear.

Yes, merge (at least via Github button) makes mess. I do not
know how well rebase will work, but probably will be better.

--
Waldek Hebisch

[Ralf Hemmecke]

> Yes, merge (at least via Github button) makes mess. I do not
> know how well rebase will work, but probably will be better.

I have seen that one now can also choose at Github whether a rebase or
merge commit will be done.

Actually, for most "rebase"-commits it will end up in a simple linear
fast-forward commit. Rebase might actually only have issues if master
has advanced since the pull request was started and the master branch
has modifications that somehow conflict with the PR. But even that can
be handled in a "rebase". I don't however know how github helps to
resolve conflicts.

Ralf

[oldk1331]

Hi Waldek and Ralf,

I have already used github webpage's rebase button, works nicely. I'll continue to do so in the future.

- Qian