Skip to content

[Merged by Bors] - chore: cleanup in Mathlib.Init#6977

Closed
kim-em wants to merge 18 commits intomasterfrom
init_cleanup
Closed

[Merged by Bors] - chore: cleanup in Mathlib.Init#6977
kim-em wants to merge 18 commits intomasterfrom
init_cleanup

Conversation

@kim-em
Copy link
Copy Markdown
Contributor

@kim-em kim-em commented Sep 6, 2023

Open in Gitpod

@kim-em kim-em added awaiting-review awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. labels Sep 6, 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 Sep 6, 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 Sep 6, 2023
@jcommelin
Copy link
Copy Markdown
Member

jcommelin commented Sep 6, 2023

Thanks 🎉

If CI passes, please remove the label awaiting-CI and merge this yourself, by adding a comment bors r+.

bors d+

@bors
Copy link
Copy Markdown

bors bot commented Sep 6, 2023

✌️ semorrison can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@github-actions github-actions bot added delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). and removed awaiting-review labels Sep 6, 2023
@kim-em
Copy link
Copy Markdown
Contributor Author

kim-em commented Sep 6, 2023

bors merge

@bors
Copy link
Copy Markdown

bors bot commented Sep 6, 2023

👎 Rejected by label

@github-actions github-actions bot added the ready-to-merge This PR has been sent to bors. label Sep 6, 2023
@kim-em kim-em removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Sep 6, 2023
@kim-em
Copy link
Copy Markdown
Contributor Author

kim-em commented Sep 6, 2023

bors merge

@kim-em
Copy link
Copy Markdown
Contributor Author

kim-em commented Sep 6, 2023

This is clashing with #6971 with bors. To save some time (they are both waiting to run), I'm just going to merge that into this PR.

@bors
Copy link
Copy Markdown

bors bot commented Sep 6, 2023

Canceled.

@kim-em
Copy link
Copy Markdown
Contributor Author

kim-em commented Sep 6, 2023

bors merge

@kim-em kim-em mentioned this pull request Sep 6, 2023
Closed
2 tasks
bors bot pushed a commit that referenced this pull request Sep 6, 2023
@kim-em
chore: cleanup in Mathlib.Init (#6977)
a226e71 
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
@bors
Copy link
Copy Markdown

bors bot commented Sep 6, 2023

Build failed (retrying...):

bors bot pushed a commit that referenced this pull request Sep 6, 2023
@kim-em
chore: cleanup in Mathlib.Init (#6977)
8ba89d8 
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
@bors
Copy link
Copy Markdown

bors bot commented Sep 6, 2023

Canceled.

@kim-em
Copy link
Copy Markdown
Contributor Author

kim-em commented Sep 6, 2023

bors p=10

bors merge

bors bot pushed a commit that referenced this pull request Sep 6, 2023
@kim-em
chore: cleanup in Mathlib.Init (#6977)
8f46576 
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
@bors
Copy link
Copy Markdown

bors bot commented Sep 6, 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 chore: cleanup in Mathlib.Init [Merged by Bors] - chore: cleanup in Mathlib.Init Sep 6, 2023
@bors bors bot closed this Sep 6, 2023
@bors bors bot deleted the init_cleanup branch September 6, 2023 23:43
ebab pushed a commit that referenced this pull request Sep 11, 2023
@kim-em @ebab
chore: cleanup in Mathlib.Init (#6977)
14661d1 
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
kodyvajjha pushed a commit that referenced this pull request Sep 22, 2023
@kim-em @kodyvajjha
chore: cleanup in Mathlib.Init (#6977)
790d920 
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). ready-to-merge This PR has been sent to bors.

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@kim-em @jcommelin