Skip to content

[Merged by Bors] - ci: add --nightlysha to create-adaptation-pr.sh#17148

Closed
jcommelin wants to merge 1 commit intomasterfrom
jmc-adaptation-pr-from-sha
Closed

[Merged by Bors] - ci: add --nightlysha to create-adaptation-pr.sh#17148
jcommelin wants to merge 1 commit intomasterfrom
jmc-adaptation-pr-from-sha

Conversation

@jcommelin
Copy link
Copy Markdown
Member


Open in Gitpod

@jcommelin jcommelin added the CI Modifies the continuous integration setup or other automation label Sep 26, 2024
@github-actions
Copy link
Copy Markdown

PR summary c1758e1980

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.

@kim-em
Copy link
Copy Markdown
Contributor

kim-em commented Sep 26, 2024

bors merge

@github-actions github-actions bot added the ready-to-merge This PR has been sent to bors. label Sep 26, 2024
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Sep 26, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title ci: add --nightlysha to create-adaptation-pr.sh [Merged by Bors] - ci: add --nightlysha to create-adaptation-pr.sh Sep 26, 2024
@mathlib-bors mathlib-bors bot closed this Sep 26, 2024
@mathlib-bors mathlib-bors bot deleted the jmc-adaptation-pr-from-sha branch September 26, 2024 08:12
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