either one of the two recent commits (d8d00318, fd97d2a7) fixed it, or there is some nondeterminism here. See #9938.