Merge master into branch?

Stream: general

[Rémy Degenne]

I have an open PR #5014 which contains a lemma that I needed at the time of writing it, but another more recent PR of mine (#5026) was merged with another more general lemma that renders the old one redundant. I want to use the new lemma, but it is not in the branch of PR #5014. What do I do? Do I just merge master into the branch of #5014 (branch Lp_space_neg_add), even if it clutters the PR with many commits from many authors? Is there a cleaner way?

Of course the best way to proceed would have been to realize first that I could write the general lemma and PR it first, but that is not what happened.

[Johan Commelin]

@Rémy Degenne You can git rebase master (after checking out your PR branch)

[Ruben Van de Velde]

If you merge master into your branch, github should only show the merge commit, not everything that landed in between

[Johan Commelin]

But merging master is also a valid option, and it means that you will not have to force-push

[Johan Commelin]

We don't really care about ugly history, it get's squashed anyway when the PR is merged into master.

[Rémy Degenne]

Ok, thanks. If merging is fine, I'll do that.

[Sebastien Gouezel]

Yes, please do merge master. And then I'll review!

[Ruben Van de Velde]

(I thought the documentation said not to rebase, but I can't find that anymore. Must've dreamed it.)

[Bryan Gin-ge Chen]

I can't remember if it's in any of our documentation, but I think the general recommendation is to avoid rebasing after people start reviewing the PR since GitHub can't put the review comments in the right place after the rebase.