Merge branch 'mg/log-decorate-HEAD'

Output from "git log --decorate" mentions HEAD when it points at a tip of an branch differently from a detached HEAD. This is a potentially backward-incompatible change. * mg/log-decorate-HEAD: log: decorate HEAD with branch name