@mauritsderuiter95 Thanks for the feedback. So this PR was not merged to master in the proposed form, but Daniel pushed a bit different commits if I read it correctly. So if the current master is ok from your point of view, the PR should be closed.
—
Reply to this email directly, view it on GitHub, or unsubscribe.
You are receiving this because you are subscribed to this thread.