Skip to content

chore: delay import of Mathlib.Tactic.Common#6971

Closed
kim-em wants to merge 15 commits intomasterfrom
delay_tactics
Closed

chore: delay import of Mathlib.Tactic.Common#6971
kim-em wants to merge 15 commits intomasterfrom
delay_tactics

Conversation

@kim-em
Copy link
Copy Markdown
Contributor

@kim-em kim-em commented Sep 6, 2023 •
edited
Loading

@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 blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Sep 6, 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 Sep 6, 2023
jcommelin
jcommelin approved these changes Sep 6, 2023
View reviewed changes
Copy link
Copy Markdown
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

@ghost ghost 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
@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 merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) labels Sep 6, 2023
@ghost
Copy link
Copy Markdown

ghost commented Sep 6, 2023

This PR/issue depends on:

@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
@kim-em
Copy link
Copy Markdown
Contributor Author

kim-em commented Sep 6, 2023

bors merge

@github-actions github-actions bot added the ready-to-merge This PR has been sent to bors. label Sep 6, 2023
bors bot pushed a commit that referenced this pull request Sep 6, 2023
@kim-em
chore: delay import of Mathlib.Tactic.Common (#6971)
b8a0658 
This slightly delays the import of Mathlib.Tactic.Common.



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
@bors
Copy link
Copy Markdown

bors bot commented Sep 6, 2023

Build failed (retrying...):

@bors
Copy link
Copy Markdown

bors bot commented Sep 6, 2023

Canceled.

@kim-em kim-em added awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. and removed ready-to-merge This PR has been sent to bors. labels Sep 6, 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 Sep 6, 2023
@kim-em
Copy link
Copy Markdown
Contributor Author

kim-em commented Sep 6, 2023

bors merge

@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 mentioned this pull request Sep 6, 2023
Closed
@kim-em
Copy link
Copy Markdown
Contributor Author

kim-em commented Sep 6, 2023

To avoid bors clashing all night, I've rolled this into #6977

@kim-em kim-em closed this Sep 6, 2023
@ChrisHughes24
Copy link
Copy Markdown
Member

ChrisHughes24 commented Sep 6, 2023

bors r-

@bors
Copy link
Copy Markdown

bors bot commented Sep 6, 2023

Canceled.

@YaelDillies YaelDillies deleted the delay_tactics branch August 12, 2025 05:35
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@jcommelin jcommelin jcommelin approved these changes

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.

3 participants

@kim-em @ChrisHughes24 @jcommelin