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.
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.