7c4d46a8d9
SVN version (r19045), but I also edited the svn:ignore to ignore these files in the same SVN commit -- I suspect that SVN got confused and did not actually delete them. This commit was SVN r19048. The following SVN revision numbers were found above: r19045 --> open-mpi/ompi@63b63d48c3