On 20.01.24 23:59, Tom Lane wrote:
> Peter Eisentraut <peter(at)eisentraut(dot)org> writes:
>> On 20.01.24 17:03, Tom Lane wrote:
>>> * I gather that the point here is to change some generated anchor
>>> tags. Would any of these tags be things people would be likely
>>> to have bookmarked?
>
>> No, because the problem is that the anchor names are randomly generated
>> in each build.
>
> D'oh. No objection then.
Thanks, committed.