Skip to content

Conversation

@jsquyres
Copy link
Member

The bot to mark Github issues as stale and/or close them does not properly handle when labels contain ":". After removing ":" from the label name on Github, update the corresponding Github Actions here to match the new label names.

The bot to mark Github issues as stale and/or close them does not
properly handle when labels contain ":".  After removing ":" from the
label name on Github, update the corresponding Github Actions here to
match the new label names.

Signed-off-by: Jeff Squyres <[email protected]>
@jsquyres jsquyres merged commit 3e82472 into open-mpi:main Feb 19, 2024
@jsquyres jsquyres deleted the pr/fix-github-issue-names branch February 19, 2024 17:58
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants