+1 looks good to me!

+1

Applied

@latkin Why not just merge PR from GitHub UI? Now it looks like a canceled PR =(.

Yep I was just going to say this.
I'm suggesting you use the automatic pull request features.

There 2 possible ways:

1. hit the merge button. (not always what you want)
2. merge the pull request manually (why did you change the commiter?) and just push. Github will detect the merge and close the PR automatically

The "merge pull request" button does a no-fast-forward merge, which isn't great IMO... So far we have been doingmerge --squash orrebase so that the history stays linear and each PR is a single commit.

In this particular case I wanted to move the commit tomaster and then merge tofsharp4 anyways, so pressing the button wouldn't have worked.

Is there a better way (besides the merge button) to close the PR so that it looks right?

I did merge it manually, but I did not see any change to this PR, so I just linked the commit and closed it.

git automatically updates the committer whenever you do rebase, etc.

Why do you prefer each PR as a single commit (just to understand the incentive)? Isn't it better to keep original commits so that we know how features are implemented incrementally?

I know this one is controversial, but the explicit merge-commit is not a bad thing because it makes the pull request visible in the git history. It allows us to find the discussion and additional information from the history/code.

regarding rebase and squash; most projects ask the author to clean up the pull request before they accept it.

I’m afraid it doesn’t work with our current codeflow. We our doing things that will make it possible eventually but right now that workflow doesn’t work for us.

Please let’s not boil the ocean, let us get a workflow that works well for us, and we can evolve it over time, as we find improvements that we like.

Kevin

From: Steffen Forkmann [mailto:notifications@github.com]
Sent: Wednesday, January 14, 2015 1:36 PM
To: Microsoft/visualfsharp
Subject: Re: [visualfsharp] Add contributing guidelines to repo root (#1)

I know this one is controversial, but the explicit merge-commit is not a bad thing because it makes the pull request visible in the git history. It allows us to find the discussion and additional information from the history/code.

—
Reply to this email directly or view it on GitHubhttps://github.com//pull/1#issuecomment-69996578.

of course. we just trying to understand.

Merge vs rebase is indeed religious war territory, don't want this to devolve into that. Single commit per PR is not uncommon - seehere,here.

I think I should have just added "Closes#1" to the message, and that would have done the auto-linkup. Totally agree that it's nice having everything linked up properly. Apologies I didn't figure that our initially, we are still GitHub n00bs.

Basically,

A gif. Finally ;-)

All is well