When merging git PRs, please use "Squash and merge" - Github makes this trivial in the UI, and it's also very easy from cmdline.
When a PR has a bunch of commits that go back and forth or include unrelated changes, we naturally don't want that superfluous state duplicated into our repos. The final changeset is what matters, and if that is good then by squashing we don't have to care how that changeset came about. This makes it easier for everyone. We don't have to nag authors to squash their repo, and authors can fix the final state by just making another commit instead of changing history in their repo. So don't care if there's 50 unrelated commits in a PR - just check if the end result is as it should be, then squash it all in. -- Tino Didriksen
_______________________________________________ Apertium-stuff mailing list Apertium-stuff@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/apertium-stuff
