On Mon, Apr 8, 2019 at 3:51 PM Stefan Seefeld <stefan@seefeld.name> wrote:

At this point in time, I'd argue...fixes, to make sure...

But soft, what commit through yonder git log states?

It is a bug, and 5e88637752ea0ecb49824904be3098656740298c is the fix!
...

To merge, or not to merge?
That is the question.

Regards