Ignore the previous patch; it didn't update EXTRA_DIST.  Use this one instead.