!2231 (comment 3043322)
Please don't merge right away, I want to check that the new CI job doesn't take too long.