Skip to content

[Merged by Bors] - fix: patch for std4#193#6188

Closed
fgdorais wants to merge 1 commit intomasterfrom
fgdorais-nat-rec
Closed

[Merged by Bors] - fix: patch for std4#193#6188
fgdorais wants to merge 1 commit intomasterfrom
fgdorais-nat-rec

Conversation

@fgdorais
Copy link
Copy Markdown
Collaborator

@fgdorais fgdorais commented Jul 27, 2023 •
edited
Loading

fix: patch for std4#193

This was just merged into Std. The Mathlib patch is very small.

Open in Gitpod

@fgdorais fgdorais added t-number-theory Number theory (also use t-algebra or t-analysis to specialize) blocked-by-batt-PR This PR depends on a PR to Batteries WIP Work in progress labels Jul 27, 2023
@ghost ghost added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Jul 27, 2023
@fgdorais fgdorais mentioned this pull request Jul 27, 2023
Merged
1 task
@fgdorais fgdorais added the t-algebra Algebra (groups, rings, fields, etc) label Jul 27, 2023
@ghost ghost added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jul 28, 2023
@ghost ghost removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jul 28, 2023
@kim-em kim-em mentioned this pull request Aug 3, 2023
Closed
@ghost ghost added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Aug 7, 2023
@ghost ghost removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Aug 15, 2023
@ghost
Copy link
Copy Markdown

ghost commented Aug 15, 2023

This PR/issue depends on:

@fgdorais fgdorais requested review from eric-wieser and kim-em August 16, 2023 01:23
@fgdorais fgdorais removed WIP Work in progress blocked-by-batt-PR This PR depends on a PR to Batteries labels Aug 16, 2023
@fgdorais
Copy link
Copy Markdown
Collaborator Author

fgdorais commented Aug 16, 2023

Having some Lake pains. I might need to fix this tomorrow. Sorry, this was supposed to be quick and easy!

@kim-em kim-em added awaiting-author A reviewer has asked the author a question or requested changes. awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. labels Aug 16, 2023
@kim-em kim-em removed their request for review August 16, 2023 04:25
@ghost ghost removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Aug 16, 2023
@github-actions github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Aug 16, 2023
@fgdorais
Copy link
Copy Markdown
Collaborator Author

fgdorais commented Aug 16, 2023

All fixed now!

@fgdorais fgdorais removed the awaiting-author A reviewer has asked the author a question or requested changes. label Aug 17, 2023
@fgdorais fgdorais mentioned this pull request Aug 17, 2023
Closed
2 tasks
@kim-em
Copy link
Copy Markdown
Contributor

kim-em commented Aug 17, 2023

bors p=10

bors merge

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Aug 17, 2023
bors bot pushed a commit that referenced this pull request Aug 17, 2023
@fgdorais
fix: patch for std4#193 (#6188)
5f5c4e1 
fix: patch for std4#193
@bors
Copy link
Copy Markdown

bors bot commented Aug 17, 2023

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

@bors bors bot changed the title fix: patch for std4#193 [Merged by Bors] - fix: patch for std4#193 Aug 17, 2023
@bors bors bot closed this Aug 17, 2023
@bors bors bot deleted the fgdorais-nat-rec branch August 17, 2023 11:16
@kim-em kim-em mentioned this pull request Aug 17, 2023
Closed
8 tasks
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@eric-wieser eric-wieser Awaiting requested review from eric-wieser

Assignees

No one assigned

Labels

ready-to-merge This PR has been sent to bors. t-algebra Algebra (groups, rings, fields, etc) t-number-theory Number theory (also use t-algebra or t-analysis to specialize)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@fgdorais @kim-em