On Mon, Jul 17, 2023 at 08:25:31PM +1000, Mark Jamsek wrote:
> :tip has the advantage of being shorter too.
> 
> However, given its behaviour you noted as resolving to the repository's
> HEAD when not in a work tree, I think it is slightly better to keep it
> as :head.
> 
> In addition, "head" is generally used in git-speak to refer to the
> branch's head meaning tip commit, so it will be familiar to that
> demographic. OTOH, "tip" is used in fossil.
> 
> I wouldn't object to the change; just expressing why I think :head is
> better suited.

Yes, let's keep :head for now then. Our documentation does use the
word "tip" in many places but let's hope users will understand that
the terms head and tip are generally interchangable.

> > In any case, I want to apply the wording change below:
> 
> ok for the diff

Thanks, committed.