[arch-dev-public] Holidays, Dec 23--Jan 8

Hi guys, I will spend my summer holidays in the wilderness and will thus be mostly unreachable from December 23 to January 8. Please do fix and/or upgrade what needs to be. Cheers. -- Gaetan