Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

chore: do not use actions-ecosystem/action-add-labels #3055

Merged
merged 4 commits into from
Dec 12, 2023

Conversation

nomeata
Copy link
Collaborator

@nomeata nomeata commented Dec 12, 2023

That action seems to be unmaintained and causes warnings
(actions-ecosystem/action-add-labels#459).

Let's just use the API directly, like we already do in
.github/workflows/labels-from-comments.yml

That action seems to be unmaintained and causes warnings
(actions-ecosystem/action-add-labels#459).

Let's just use the API directly, like we already do in
`.github/workflows/labels-from-comments.yml`
@nomeata nomeata requested review from Kha and kim-em as code owners December 12, 2023 21:43
@nomeata nomeata marked this pull request as draft December 12, 2023 21:49
This reverts commit 84ef8d6.
@nomeata nomeata marked this pull request as ready for review December 12, 2023 21:55
@nomeata nomeata added the will-merge-soon …unless someone speaks up label Dec 12, 2023
@github-actions github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Dec 12, 2023
@leanprover-community-mathlib4-bot
Copy link
Collaborator

  • ❗ Mathlib CI will not be attempted unless you rebase your PR onto the 'nightly' branch. (2023-12-12 22:12:29)

@kim-em kim-em added this pull request to the merge queue Dec 12, 2023
Merged via the queue into master with commit de7d78a Dec 12, 2023
8 checks passed
@nomeata nomeata deleted the joachim/pr-release-label branch December 13, 2023 07:33
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN will-merge-soon …unless someone speaks up
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants