Closed jan-ferdinand closed 9 months ago
Due to my force-push, the GitHub indicator erroneously marks this branch as closed, not merged. The change discussed herein first appeared on branch master
in commit d7ac0c3c18c97bf3f39812a6b0dddafee6b13c19.
In spirit equivalent to #75. I suggest to use this PR instead. Notable differences: