Merge pull request 'Node page Discord picker: org's servers + voice channels, not raw IDs (#213 item 3)' (#220) from feat/213-node-join-picker into main
Build & Deploy / Build & push images (push) Successful in 4m58s
Build & Deploy / Deploy Firestore rules & indexes (push) Successful in 29s
Build & Deploy / Deploy to VM (push) Successful in 2m37s
Build & Deploy / Report a failed deploy (push) Skipped

Reviewed-on: #220
This commit was merged in pull request #220.
This commit is contained in:
2026-10-04 22:05:49 -04:00
11 changed files with 1230 additions and 104 deletions
+1
View File
@@ -16,6 +16,7 @@ class DRBBot(commands.Bot):
await self.load_extension("app.commands.radio")
await self.load_extension("app.commands.drb")
await self.load_extension("app.commands.trips")
await self.load_extension("app.commands.directory")
if settings.dev_guild_id:
guild = discord.Object(id=settings.dev_guild_id)