20 Oct
2023
20 Oct
'23
7:31 p.m.
A few recent changes broke the macOS build. Unfortunately nobody noticed, because the macOS CI job always fails. :-(
However, we can still fix that. I'm not sure that the second commit is the best approach, would like to have comments from Henri.