Skip to content

[Merged by Bors] - fix: remove remaining ^ fixes#8463

Closed
kmill wants to merge 2 commits intomasterfrom
kmill_remove_2220_fixes
Closed

[Merged by Bors] - fix: remove remaining ^ fixes#8463
kmill wants to merge 2 commits intomasterfrom
kmill_remove_2220_fixes

Conversation

@kmill
Copy link
Copy Markdown
Contributor

@kmill kmill commented Nov 17, 2023


Open in Gitpod

@PatrickMassot
Copy link
Copy Markdown
Member

bors merge

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Nov 18, 2023
mathlib-bors bot pushed a commit that referenced this pull request Nov 18, 2023
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Nov 18, 2023

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title fix: remove remaining ^ fixes [Merged by Bors] - fix: remove remaining ^ fixes Nov 18, 2023
@mathlib-bors mathlib-bors bot closed this Nov 18, 2023
@mathlib-bors mathlib-bors bot deleted the kmill_remove_2220_fixes branch November 18, 2023 02:08
alexkeizer pushed a commit that referenced this pull request Nov 21, 2023
grunweg pushed a commit that referenced this pull request Dec 15, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

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