Minor change to delete git conflict.

A git conflict was left over from a previous merge, which was not taken
care of by git mergetool.