That adds 4.1 MiB, but it saves user headaches, so I think it’s worth it.

I’ll go ahead and push that if there are no objections.

Thanks,
Ludo’.