On Mon, Mar 11, 2024 at 1:27 PM Moin Rahman <b...@freebsd.org> wrote: > > Github PRs are mostly ignored as those cannot be merged there.
Not really, there is a lot of stuff coming from GitHub. Yes, you can't merge them via web UI, but it is still simple with gh CLI. I do merge contributions from GitHub from time to time.
