If I rename a repository in GitHub, the repository still has the old name in the Bors dashboard. Is there a way to rename the repository in Bors?
You're right... there's no actual way in there to do so.
It's pretty clear where in the code it should go. You would add it to synchronize_project, so that the name would get updated at the same time the repository admin clicked "synchronize pull requests". But that's not actually there right now.
If you're looking for a workaround right now, you'd have to remove the repository from the GitHub app, then add it back again.
1 Like
Yeah, I ended up removing Bors from the repository and then reinstalling Bors on that repository.
It would be nice to eventually have the functionality built in as you described. Unfortunately I don't currently have the time to work on it.