Closed andresmmera closed 6 years ago
I had to remove the last commit from @felix-salfelder to cherry-pick 933415e6a171bacd1bf8de79b4491772a9f33d35 here, otherwise, an additional commit for a merge was needed... and basically, both commits do the same thing
This PR is a cherry pick of ecae7fa and d30dc6d targeted to develop.
As @in3otd said here, these commits need to be merge into develop. Then, we need to rebase and merge #871. Otherwise develop and release-0.0.20 will remain broken.