> This issue is about clarifying which head we are talking about for
> future generations. So why not just "4.7 HEAD" or "5.0 HEAD"?
> It would contract to something cutesie like 4.7H, 5.0H of course.

Again, as 5 people already stated, until 3 weeks ago we didn't know
wether what is now known as 5.0 would be 4.8 or 5.0.