Case sensitivity when deleting a checked out branch

Hello,

I came across an odd behavior in Git related to case sensitivity when 
deleting a checked out branch.
I was not able to find much information about it.

$ git checkout -b foo
$ git branch -d foo       # error: Cannot delete branch 'foo' checked 
out => this is expected, nothing happens since you are on branch 'foo'
$ git branch -d Foo       # Deleted branch Foo => this is not expected, 
Git removed 'foo' from .git/refs/heads

Git removed the 'foo' file from .git/refs/heads, but did not update the 
.git/HEAD file which still contains "ref: refs/heads/foo".

In fact, everything looks like a "git checkout --orphan foo":
$ git status              # On branch foo. No commits yet (the working 
tree is staged)
$ git log                 # fatal: your current branch 'foo' does not 
have any commits yet
$ git rev-parse HEAD --   # fatal: bad revision 'HEAD'
$ git fsck                # notice: HEAD points to an unborn branch (foo)

You can run "git checkout <other_branch>" to get back on your feet as 
you would after "git checkout --orphan foo".

The thing is, you get there unexpectedly without any warning, just with 
a case sensitivity mistake in "git branch -d".
Even it is seems unlikely to happen, someone ran into this at my job.

Tested on Windows 2.15.1.windows.2 and 2.16.2.windows.1, and on Mac OS 
(I think it was a 2.14 version).

Best regards,
Guillaume

---
L'absence de virus dans ce courrier électronique a été vérifiée par le logiciel antivirus Avast.
https://www.avast.com/antivirus