On Tue, 6 Jul 2021 at 06:55, James Coleman <jtc331(at)gmail(dot)com> wrote:> While re-reading this code I found a small typo and fixed it (making> the comment more explicit at the same time).
Thanks. Pushed (9ee91cc58).
David