Closed Ghazi-Bouabene closed 5 years ago
@Ghazi-Bouabene Could that fix go in the 0.13 release?
@marcelluethi No. This fix is meant for features that have been merged into develop only today (PRs that have been approved since a while but merged only today). So these features are not in the release branch. Also, given that they have not been tested, I would include them only in the next release.
I haven't tested it, but yeah, looks good to me as well, thanks :)
Following Mr. Langguth's good suggestion :)