On Tue, Feb 24, 2026 at 5:40 PM Markus Graf <[email protected]> wrote:
>
> Is one PR on github ok or should I submit one per port?

One PR is certainly fine, you can just put each port into a separate commit.

Reply via email to