On 7/8/22 15:01, Michal Privoznik wrote: > Ping? Might be worth merging before tomorrow's freeze. Michal