closed with commit 75896498
mentioned in commit 75896498
By Rémi Cresson on 2022-09-29T10:25:20 (imported from GitLab)