Python: rename file in Windows

Observation: function os.remove under Windows doesn't allow to overwrite an existing file. Python from Cygwin works properly.

Here is a workaround:

def rename_file(old, new):
    if sys.platform != 'win32':
        os.rename(new, old)
    else:
        os.remove(old)
        os.rename(new, old)