<div dir="ltr"><div>I have a failure here but I can't see what the problem is:</div><div><br></div><a href="https://gitlab.com/petsc/petsc/-/jobs/755956828">https://gitlab.com/petsc/petsc/-/jobs/755956828</a><br><div><br></div><div>Am I missing something?</div><div><br></div><div>Thanks,</div><div>Mark</div></div>