Andreas gave me permission to push to this repository, so I pushed a fix
to this bug in branch bug-e5f3dfc055c.  The fix is based on the patch that
I attached earlier.