On 6/22/25 9:21 PM, izzy Meyer wrote:
> Here's a new port with these changes.

I still think it should be extensible (= you can add extensions)
instead of extendable/extendible (= it can be made bigger). But be
that as it may.

ok volker@

> Good to merge?

New ports need two ok's, so halfway there :-)