On Thu, Jul 8, 2021 at 8:48 AM Daniel Gustafsson <[email protected]> wrote: > > On 3 Jun 2021, at 04:07, Thomas Munro <[email protected]> wrote: > > Here's a patch to remove the misleading comments. > > While not an expert in the area; reading the referenced commit and the code > with the now removed comments, I think this is correct.
Thanks! I made the comments slightly more uniform and pushed.
