Add a Git_ext Copy operation to copy (and eventually edit afterwards)

[hannesm]

The reasoning is that, as far as I can tell, there can be git diffs where a file is copied and afterwards modified. This means the common Edit operation doesn't fully fit.

One such example is #43

This needs some attention from @kit-ty-kate @shym and maybe @edwintorok

[hannesm]

As suggested in #43, this needs some tests, and it also doesn't feel very principled:

• is it fine to skip (without warning) a hunk that has already been applied?
• is the git copy operation really needed? Is the semantics of Edit really if a and b are different to remove a after the operation?
• In opatch, the let create = ... in now looks very hand-wavy, it would be nice to have a better story there.

[edwintorok]

See #43 (comment), I've found some documentation on how this is supposed to work in git diff, but implementing that in opatch would be tricky, because it'd require preserving all the original files, in particular there is this bit of non-POSIX behaviour:

All the file1 files in the output refer to files before the commit, and all the file2 files refer to files after the commit. It is incorrect to apply each change to each file sequentially