On Mon, Jan 05, 2026 at 03:30:43PM +0700, John Naylor wrote:
> I suspect it doesn't make much difference in the grand scheme of
> things, but the code has to do either one thing or the other, so +1 to
> do the more sensible thing.
Thanks for the input. I have applied the change as 68119480a763 on
HEAD, after adding a comment to document the expectation.
--
Michael