overwritten. These modifications were accepted as PR#741 but somehow I
  clobbered them when PR#742 was merged. There was some unintentional overlap in
  my local repository that I didn't straighten out before pushing.