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