Re: Amending commits

[Gregory Heytings]

> > > > 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.