On 21.11.23 14:23, Peter Eisentraut wrote:
> On 21.11.23 02:56, Andres Freund wrote:
>> One remaining question is whether we should adjust
>> install-doc-{html,man} to
>> be install-{html,man}, to match the docs targets.
>
> Ah didn't notice that one; yes please.
I think this was done?