git may delete current branch on case insensitive file system (Mac)

This was a fun one. I accidentally upcased the first letter of a branch beginning with "d" instead of upcasing the -d option as I had intended, with a surprising result (Mac OS). Easily reproduced:

% git checkout -b dummy Switched to a new branch 'dummy' % git branch -d dummy error: cannot delete branch 'dummy' used by worktree at '/Users/riccar/...' % git branch -D dummy error: cannot delete branch 'dummy' used by worktree at '/Users/riccar/...' % git branch -d Dummy Deleted branch Dummy (was c32dfb2). % git log fatal: your current branch 'dummy' does not have any commits yet

On Linux, you instead get

% git branch -d Dummy error: branch 'Dummy' not found

        /Richard