@elextr @kugel- Thanks a lot for your votes, then we will go with 3.

@elextr However, I feel it would make more sense for me to create a new branch (and so a new PL) for that, since it is more a fix than a feature and so the original changes would be kept. Would that be okay?

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