Hello, наб, le sam. 04 juil. 2020 13:32:35 +0200, a ecrit: > I've posted these patches to debian-boot@ last month, > but thought I'd try again. Thanks for the ping. Since there was no concern raised in the meanwhile, I have pushed the change to the gits. Samuel