If your patch doesn't make it in within 48 hours please post
> here with a complaint.
OK, I committed it. In addition to the files you modified, you should
consider CHANGELOG and API_CHANGES. The former for non-trivial
commits, the latter for API_CHANGES. With this commit, I made an
entry to CHANGELOG.
Many thanks,
JDH