Skip to content

[Merged by Bors] - chore: avoid Ne.def (adaptation for nightly-2024-03-27)#11813

Closed
Ruben-VandeVelde wants to merge 1 commit intomasterfrom
2024-03-27-prep-ne
Closed

[Merged by Bors] - chore: avoid Ne.def (adaptation for nightly-2024-03-27)#11813
Ruben-VandeVelde wants to merge 1 commit intomasterfrom
2024-03-27-prep-ne

Conversation

@Ruben-VandeVelde
Copy link
Copy Markdown
Contributor

@Ruben-VandeVelde Ruben-VandeVelde commented Mar 31, 2024


Extracted from #11735; follow on from #11801.

Open in Gitpod

@eric-wieser
Copy link
Copy Markdown
Member

Does this follow on from #11801? If so, please put that in the description.

@Ruben-VandeVelde
Copy link
Copy Markdown
Contributor Author

Yes, sorry, I thought I'd mentioned that.

@j-loreaux
Copy link
Copy Markdown
Contributor

bors merge

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Apr 1, 2024
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Apr 1, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title chore: avoid Ne.def (adaptation for nightly-2024-03-27) [Merged by Bors] - chore: avoid Ne.def (adaptation for nightly-2024-03-27) Apr 1, 2024
@mathlib-bors mathlib-bors bot closed this Apr 1, 2024
@mathlib-bors mathlib-bors bot deleted the 2024-03-27-prep-ne branch April 1, 2024 18:06
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.

4 participants