Posted By: Anonymous
I think it should work to copy the directory to be renamed to a new directory with desired name, and delete the old directory, and
git commit and
push everything. But is this the best way?
Basic rename (or move):
git mv <old name> <new name>
Case sensitive rename—eg. from
CaseSensitive—you must use a two step:
git mv casesensitive tmp git mv tmp CaseSensitive
…followed by commit and push would be the simplest way to rename a directory in a git repo.