[OMPI devel] GitHub v4.0.2 tag is broken

[Geoffrey Paulsen via devel]

Ben,

  Oops, looks like I may have pushed a v4.0.2 branch around March 10th.
  Fortunately the v4.0.2 tag is fine and unaltered.
  I've deleted the v4.0.2 branch.  Thanks for bringing this to our attention.

  Geoff Paulsen