Re: [petsc-dev] --known-mpi-shared-library and --with-batch annoyance