Hey folks This is getting ridiculous - we have PRs sitting on GitHub that are more than a year old! If they haven’t been committed in all that time, they can’t possibly be worth anything now.
Would people _please_ start paying attention to their PRs? Either close them, or update/commit them. Ralph _______________________________________________ devel mailing list devel@lists.open-mpi.org https://lists.open-mpi.org/mailman/listinfo/devel
