On 20.01.24 23:59, Tom Lane wrote:
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.
Thanks, committed.
