Skip to content

Update to /repos command group - #135

Draft
49Indium wants to merge 4 commits into
mainfrom
repos
Draft

Update to /repos command group#135
49Indium wants to merge 4 commits into
mainfrom
repos

Conversation

@49Indium

@49Indium 49Indium commented Jul 2, 2023

Copy link
Copy Markdown
Member

A few changes to the /repos command group:

  • Changed list and find to run as embeds
  • Added issues, which lists the issues of a specific repo
  • Added prs, which lists the PRs of a specific repo

This will require a new auth token in the bot for github API access, which is given by an environment variable. I will update the wiki soon.

@ndrwbrwn ndrwbrwn left a comment

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM. Awaiting committee discussion on setting up a token.

Be aware that this is a Recurring Task:tm: that will need to be managed by future committees. Github tokens are inherently temporary; there will come a time when the token dies and whoever is around then will need to know what's going on.

@ndrwbrwn
ndrwbrwn marked this pull request as draft October 28, 2023 02:16
@ndrwbrwn

Copy link
Copy Markdown
Member

Also converted to draft while we figure out what to do with tokens.

@ndrwbrwn ndrwbrwn added the awaiting-discussion needs infra/committee discussion to progress label Oct 28, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

awaiting-discussion needs infra/committee discussion to progress

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants