I have uninstalled the public installation of Bors from my GitHub organizations
aluthge-edu, because I am planning on installing self-hosted installations of Bors on those two organizations.
However, four repositories in the
aluthge-edu organizations still show up on the https://app.bors.tech/repositories page:
- aluthge/DelayedErrors.jl - https://app.bors.tech/repositories/12701
- aluthge/OfflineRegistry - https://app.bors.tech/repositories/12700
- aluthge/PredictMD-docker - https://app.bors.tech/repositories/12699
- aluthge-edu/test-repo-edu-bors - https://app.bors.tech/repositories/19306
How can I remove these repositories from my dashboard and from the public installation of Bors?
Okay, they're gone (I just removed them by hand).
It's actually kind of annoying that I overlooked it. There's a button for syncing all of the repositories, and it'll even identify and add new ones, but it won't automatically remove old ones...
By the way, since you had removed them from GitHub, the public instance's access to those repos had been revoked. It wasn't going to do any harm; just take up space.
Should we fix that? Like you said, it's not a big deal since leaving those repos doesn't do any harm, but it is a little inconvenient to have them taking up space in the dashboard.
How difficult would it be to modify the "button for syncing all of the repositories" to add functionality for automatically removing old repositories?
It wouldn't be horribly difficult, but it would require some work. Right now, it basically loops through all of the installations in the database, but we need it to actually pull a list of all installations from the GitHub API, and it needs to compare both lists.