Closed KrisThielemans closed 1 week ago
Fixes #907
This fixes the build jobs, but the devel jobs are not run (I don't understand the logic there), so I don't know if they are broken now. I'll just merge...
build
devel
success 😄
Fixes #907