Merge fails if you delete a file remotely, and edit it locally

[jdmansour]

Unfortunately I've found another problem in the merge logic. Our users seem to have a talent for hitting wierd edge cases.

Bug description

When you delete a file on the remote, and at the same edit the file locally, you can end up with diverged branches:

Expected behaviour

It should keep the local change, since we never delete the student's work.

Actual behaviour

We get a merge conflict:

puller: $ git -c [email protected] -c user.name=nbgitpuller merge -Xours origin/master
puller: CONFLICT (modify/delete): README.md deleted in origin/master and modified in HEAD. Version HEAD of README.md left in tree.
puller: Automatic merge failed; fix conflicts and then commit the result.

How to reproduce

1. Check out a repository with some files via nbgitpuller
2. Delete one file in the repository, commit and push
3. Edit the file on the JupyterHub instance
4. Click the nbgitpuller link again.

I've also added a test for this here: https://github.com/jdmansour/nbgitpuller/tree/wip-modify-delete-conflict . The test fails both before and after my recent patches.

In this case I don't really know how to resolve it. git merge -Xours can't deal with delete/modify conflicts. One thing we could do is to detect the error case, and then manually resolve the conflict by git adding the local file. I'm not sure there is a way to prevent this case before the merge.