Resolving pull request conflicts

[Mojca Miklavec]

On 23 February 2017 at 11:19, Ryan Schmidt wrote:
> GitHub invited me to edit the file on the web to resolve the conflict, so I did. I was then asked by the PR author not to do that.

To avoid confusion about my earlier replies: the only part that's in
my opinion non-desirable is ending up with lots and lots of merge
commits in master. Nothing else.

(If merge is required as an intermediate step to help people achieve
the goal faster and more efficient, I don't see a problem. Before or
once it ends up in master, linear history would be preferable.)

Mojca