@vanrein Thank you for the pull request. It is a bit more complicated one, and it was also not clear to me if the work from your side was already done, as there was an extensive discussion in #3119. Also summer time probably plays a role, with several developers out of the office for some time. I will review it this week and if there are not other comments or objections, probably merge it.

Its always good to send a quick ping if you do not get a reply to a PR for some reasons. Looking forward to other contributions from your side.

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