Known problem.  I believe it's not easy to fix, though, so we won't
bother for now.