We have so far only had a request to rename a single repo. Add this repo
rename to our record keeping here to track for the future. Please do not
merge this until after the rename has been completed.
Change-Id: Ided161c7afa9c232ddc498c7542c8fc0bbd5c5d0