Peter Eisentraut <[email protected]> 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.
regards, tom lane
