<3648ab81-8216-4fb3-82dd-846774f3ad16@www.fastmail.com>
Sorry for spamming the list. I did some things wrong when trying to fix the patch. I am not familiar with the email-based workflow and I don't know how to delete those embarrassing mistakes. This patch should be the latest change.