Skip to content

[Merged by Bors] - fix(update_dependencies.yml): restore order of install elan and checkout repo#16366

Closed
bryangingechen wants to merge 1 commit intomasterfrom
bgc-fix-update-dependencies-elan-init
Closed

[Merged by Bors] - fix(update_dependencies.yml): restore order of install elan and checkout repo#16366
bryangingechen wants to merge 1 commit intomasterfrom
bgc-fix-update-dependencies-elan-init

Conversation

@bryangingechen
Copy link
Copy Markdown
Contributor

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.


Open in Gitpod

@github-actions
Copy link
Copy Markdown

PR summary a59a26f288

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.

Copy link
Copy Markdown
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

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

Thanks 🎉

bors merge

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.
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Aug 31, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title fix(update_dependencies.yml): restore order of install elan and checkout repo [Merged by Bors] - fix(update_dependencies.yml): restore order of install elan and checkout repo Aug 31, 2024
@mathlib-bors mathlib-bors bot closed this Aug 31, 2024
@mathlib-bors mathlib-bors bot deleted the bgc-fix-update-dependencies-elan-init branch August 31, 2024 14:58
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
…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
…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

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants