Closed GernotMaier closed 6 years ago
@GernotMaier - Could you please finalise this PR? This is a very large and good changeset, and only two very small points remain and then this can go in. As a reviewer it's always hard to come back to something after a long time, and I'm going on vacation soon.
@GernotMaier - merge?
First of all: apologies for the super-slow reaction - was simply flooded with too many things.
yes, please merge.
@GernotMaier - Thanks!
This pull request contains:
The last point probably breaks the pull request, but hopefully helps with the discussion on how to move forward with such sources.