This serves in lieu of a pull request, which github is having trouble
generating.