-
Fix Windows file case changing · 8cde69f5Hein-Pieter van Braam authored
Windows APIs don't really provide a way to change a filename case. This implements a little juggling to make this work. We first create a guaranteed unique temporary file, we then replace the original file with the temporary file and we finally rename it to the desired filename case. (cherry picked from commit d69d58deeaa523c6c38958b3956423ae8f814909)
8cde69f5
×