Any estimate when that might be? Any chance that a group of people could do the merging in the meantime, rather than just Stefan? Right now the last PR in General was merged more than 13 hours ago.
When we’re more confident that the results are always correct. As to more people doing merges, there are a number of people with permissions. I’ll look into making sure those who know how to review these things are aware that they can merge PRs.