On Tue, Dec 14, 2021 at 12:47 PM Mario Carneiro <[email protected]> wrote:
> One thing that I think we should stick to is one commit per PR. We had a > similar discussion for metamath-knife but for set.mm it's important to > keep PR sizes down so that people can reasonably review them, and squash > merges keep things organized. This is the mechanism we've been using in > mathlib and it works well to avoid merge conflicts, especially when things > scale to many concurrent PRs. > For big PRs that benefit from multiple commits, I think the commits should be consciously organized, squashing away bugfix commits and rebasing (not merging) on master. Such PRs are merged using the "rebase" option instead of "squash", but "squash" should be the default (and "merge" should not be used). -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJSsDeUTNiUSskCMh6Gzuk5ZvqG29LkqPQV-RiS9nMQ04RQ%40mail.gmail.com.
