On Tue, 2025-03-04 at 16:23 -0500, Robert Haas wrote:
> But, I'm doubtful that
> letting unrelated extensions try to share the same option name is
> that
> thing.
This sub-discussion started because we were wondering whether to prefix
the options. I'm just pointing out that, even if there is a collision,
and it happened to work, it's as likely to be a feature as a bug.
I didn't look into the technical details to see what might be required
to allow that kind of collaboration, and I am not suggesting you
redesign the entire feature around that idea.
Regards,
Jeff Davis
