On Fri, Jun 13, 2025 at 09:03:07AM +0100, John Garry wrote: > I suppose that many comments in 1/2 aren't relevant any more from this > change. What do you mean with comments in 1/2?