>>>> Just try it yourself.  git push origin --delete master, git config 
>>>> receive.denyDeleteCurrent ignore, git push origin --delete master.
>>>
>>> So this is a documentation bug.
>>
>> Or an understanding bug 😉 All Git repositories have a "current" 
>> branch,
>
> This is irrelevant, because the documentation explicitly excludes bare 
> repositories.
>

Does it?  What I see is that it explains the meaning to that option for 
non-bare repositories, but doesn't say anything, and does not explicitly 
exclude anything, for bare repositories.