merge

2017-10-08 git: mergetool outputs 'No files need merging' while git rerere enabled