On Wed, Oct 04, 2023 at 05:00:26PM +0200, Alvaro Herrera wrote:
> On 2023-Oct-04, Robert Haas wrote:
>
>> The original issue I reported does make a real difference, though. :-)
>
> Yes, absolutely, and I agree that it'd be better to get it fixed.
Here's a patch. I didn't address the class="parameter" stuff at all. I
figured it would be best to handle that separately.
--
Nathan Bossart
Amazon Web Services: https://aws.amazon.com