On Thu, Jul 16, 2020 at 5:10 PM Wolfgang Corcoran-Mathe <xxxxxx@sigwinch.xyz> wrote:

Sounds good. If Arthur will accept it, I'll send a PR removing them.

Since both authors were surprised by the behavior under these circumstances, it definitely counts as an error, so I have to say yes to an erratum.