On Friday, 10 February 2017 at 17:15:12 UTC, Dominikus Dittes Scherkl wrote: > Hmm. For me seems like you got some comments on your PR but > didn't answer. Seems plausible not to include such PR. Ah, you received those answers just now, not at that time. Sorry.