On Mon, Apr 8, 2019 at 3:51 PM Stefan Seefeld 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