Katsumi Yamaoka <yamaoka@jpl.org> writes:

> The change 72166f2f3dba18f1217c666574032f5a0351ed65 seems to have
> fixed this bug.

I'm closing it then.