<div dir="ltr">I would like to merge <div><br></div><div><div><a href="https://bitbucket.org/petsc/petsc/branch/stefano_zampini/matmumps-schursupport">https://bitbucket.org/petsc/petsc/branch/stefano_zampini/matmumps-schursupport</a><br></div><div><br></div><div>into next. Any objection? I will open a PR in that case and we can discuss.</div><div><br></div>-- <br><div class="gmail_signature">Stefano</div>
</div></div>