There have been no comments about this problem since Michael Vogt's changes were committed, so I'm marking this as Fix Released. Thanks for your report.
There have been no comments about this problem since Michael Vogt's changes were committed, so I'm marking this as Fix Released. Thanks for your report.