Изменить регистр имени папки в Git

Приключилась ситуация, когда в репозиторий часть файлов записалась в папку Gedemin, а часть -- в gedemin. После этого, на диске во Windows мы видим одну папку -- Gedemin, поскольку операционная система не чувствительна к регистру имен файлов, а в веб интерфейсе github-a -- две. Это не смертельно, но по крайней мере некрасиво. Исправить ситуацию поможет следующая последовательность команд:

git config core.ignorecase false
git mv gedemin tmp
git mv tmp Gedemin
git add -u Gedemin
git commit -m "Changed folder name case"
git config core.ignorecase true