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, 
unless they are in a "detached HEAD" state.  Again, a bare repository has 
a current branch: it's the branch that you get when you clone it.  And 
"git branch" works in a bare repository, too: you'll see a star in front 
of is "current" branch. The documentation could be more explicit indeed, 
but what would be the meaning of receive.denyDeleteCurrent in a bare 
repository?