printf_("%#.4o", 1) produces "00001", should produce "0001"

[eyalroz]

According to cppreference.com, and as implemented in glibc, the alternative mode for %o must ensure at least one leading zero is printed - but it doesn't increase the precision if a leading zero is already printed. Thus,

printf_("%#.4o", 1)

must produce "0001", not "00001". And yet - the latter is produced.