Commit 8d6552396ceae7736522c86dbef812e12bb1968f

Edward Thomson 2015-01-16T18:37:06

checkout: remove files before writing new ones On case insensitive filesystems, we may have files in the working directory that case fold to a name we want to write. Remove those files (by default) so that we will not end up with a filename that has the unexpected case.