We want to cleanup our GitHub tokens, and this repo is different from all others by historical accident.