Hein-Pieter van Braam 8cde69f5f2 Fix Windows file case changing ...

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 d69d58deea)

2018-02-24 18:09:20 +01:00

9.7 KiB

Raw Blame History

View Raw