Note that the Hydra coverage job builds with precompiled headers disabled, so it should catch this.

I think the GitHub CI does too, in which case the issue must be something like master changing from when the CI was run. Nevermind! Would you be opposed to making PR CI do so? I would prefer catching this earlier than later, especially because when I merge master into my branches our own CI does build coverage and so will fail.

I removed the WIP from this in any case, now that I verified the coverage job myself.

Maybe it would be better to just disable precompiled headers in the regular job. Running coverage just for that would be a bit expensive.

I'll look into that, then.