Merge branch 'da/mergetool-temporary-filename'

Tweak the names of the three throw-away files "git mergetool" comes up with to feed the merge tool backend, so that a file with a single dot in its name in the original (e.g. "hello.c") will have only one dot in these variants (e.g. "hello_BASE_4321.c"). * da/mergetool-temporary-filename: mergetool: use more conservative temporary filenames