On Thursday, 12 December 2024 at 08:31:00 UTC, Mike Parker wrote:
Second, the PR for the ARM backend was a diff of over 5000 LOC and was practically unreviewable. He'd talked with Dennis about merging it even though it wasn't yet a functioning backend. He continually rebased it, but it was hard for anyone to follow his progress because he kept adding to this gigantic PR. He thought it would be better if it were mainlined.
It should be merged. Things rotting in PRs is absolutely disastrous.
