On Sat, 30 Sept 2023 at 10:21, Darrick J. Wong <djwong@xxxxxxxxxx> wrote: > > Doh, wrong repo. I'm kinda surprised that git request-pull didn't > complain about that. I suspect it did complain, but that one-liner is admittedly much too easy to overlook when everything else looks sane. > Will send a new one. Thanks, pulled. Linus