Ok, I have created two separate PRs:

Unfortunately, github does not allow me to create the second one in this repository, because it compares two branches in forked repository. But I'll move it here as soon as possible, as explained in the first PR.

I will close this PR, as it is superseded by the two linked above.

—
You are receiving this because you are subscribed to this thread.
Reply to this email directly, view it on GitHub, or unsubscribe.