On Mon, 29 Aug 2022 13:51:13 +0200, =?utf-8?B?0L3QsNCx?= wrote:

> In that case, how about this scissor-patch?
> It has the added benefit of removing the existing floating-point usage.

That version looks good to me, committed.

 - todd

Reply via email to