Hi there Samuel, I did supersede your MP with the additional commit that fixes the build problem. I cherry-picked your commit to keep all your work intact. It was necessary since neither of the two fixes can produce a green CI job alone. There are intermittent issues with the CI, which should hopefully be resolved today and this will get merged.
Hi there Samuel, I did supersede your MP with the additional commit that fixes the build problem. I cherry-picked your commit to keep all your work intact. It was necessary since neither of the two fixes can produce a green CI job alone. There are intermittent issues with the CI, which should hopefully be resolved today and this will get merged.
Thanks for the patch.