Skip to content

[Merged by Bors] - fix(update_dependencies.yml): do not run if the PR already has the ready-to-merge label#16335

Closed
bryangingechen wants to merge 1 commit intomasterfrom
bgc-update-dependencies-label
Closed

[Merged by Bors] - fix(update_dependencies.yml): do not run if the PR already has the ready-to-merge label#16335
bryangingechen wants to merge 1 commit intomasterfrom
bgc-update-dependencies-label

Conversation

@bryangingechen
Copy link
Copy Markdown
Contributor

This should prevent cases where the bot repeatedly cancels bors batches as in #16286


Open in Gitpod

…ady-to-merge label

This should prevent  cases where the bot repeatedly cancels bors batches as in #16286
@bryangingechen bryangingechen added the CI Modifies the continuous integration setup or other automation label Aug 30, 2024
@github-actions
Copy link
Copy Markdown

PR summary 900eabf031

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

fetch-depth: 0
token: "${{ secrets.NIGHTLY_TESTING }}"

- name: Get PR and labels
Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

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

I copied this step from our main build.yml.in file, where it's used to check if "auto-merge-after-CI" is present.

@kim-em
Copy link
Copy Markdown
Contributor

kim-em commented Aug 30, 2024

bors merge

@github-actions github-actions bot added the ready-to-merge This PR has been sent to bors. label Aug 30, 2024
mathlib-bors bot pushed a commit that referenced this pull request Aug 30, 2024
…ady-to-merge label (#16335)

This should prevent cases where the bot repeatedly cancels bors batches as in #16286
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Aug 30, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title fix(update_dependencies.yml): do not run if the PR already has the ready-to-merge label [Merged by Bors] - fix(update_dependencies.yml): do not run if the PR already has the ready-to-merge label Aug 30, 2024
@mathlib-bors mathlib-bors bot closed this Aug 30, 2024
@mathlib-bors mathlib-bors bot deleted the bgc-update-dependencies-label branch August 30, 2024 23:47
mathlib-bors bot pushed a commit that referenced this pull request Aug 31, 2024
…out repo (#16366)

In #16335, I swapped the order of checking out the repo and installing `elan`. That seems to have caused the bot to try to push `elan-init` to `master` in #16360. I've reverted that here.
joneugster pushed a commit that referenced this pull request Aug 31, 2024
…ady-to-merge label (#16335)

This should prevent cases where the bot repeatedly cancels bors batches as in #16286
bjoernkjoshanssen pushed a commit that referenced this pull request Sep 9, 2024
…ady-to-merge label (#16335)

This should prevent cases where the bot repeatedly cancels bors batches as in #16286
bjoernkjoshanssen pushed a commit that referenced this pull request Sep 9, 2024
…out repo (#16366)

In #16335, I swapped the order of checking out the repo and installing `elan`. That seems to have caused the bot to try to push `elan-init` to `master` in #16360. I've reverted that here.
bjoernkjoshanssen pushed a commit that referenced this pull request Sep 9, 2024
…ady-to-merge label (#16335)

This should prevent cases where the bot repeatedly cancels bors batches as in #16286
bjoernkjoshanssen pushed a commit that referenced this pull request Sep 9, 2024
…out repo (#16366)

In #16335, I swapped the order of checking out the repo and installing `elan`. That seems to have caused the bot to try to push `elan-init` to `master` in #16360. I've reverted that here.
bjoernkjoshanssen pushed a commit that referenced this pull request Sep 12, 2024
…ady-to-merge label (#16335)

This should prevent cases where the bot repeatedly cancels bors batches as in #16286
bjoernkjoshanssen pushed a commit that referenced this pull request Sep 12, 2024
…out repo (#16366)

In #16335, I swapped the order of checking out the repo and installing `elan`. That seems to have caused the bot to try to push `elan-init` to `master` in #16360. I've reverted that here.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

CI Modifies the continuous integration setup or other automation ready-to-merge This PR has been sent to bors.

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants