Skip to content

[Merged by Bors] - chore: implement simp_rw config matching better#8592

Closed
alexjbest wants to merge 1 commit intomasterfrom
alexjbest/simprw2
Closed

[Merged by Bors] - chore: implement simp_rw config matching better#8592
alexjbest wants to merge 1 commit intomasterfrom
alexjbest/simprw2

Conversation

@alexjbest
Copy link
Copy Markdown
Member


Open in Gitpod

@alexjbest alexjbest added awaiting-review t-meta Tactics, attributes or user commands awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. labels Nov 23, 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 Nov 23, 2023
@robertylewis
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 26, 2023
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Nov 26, 2023

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title chore: implement simp_rw config matching better [Merged by Bors] - chore: implement simp_rw config matching better Nov 26, 2023
@mathlib-bors mathlib-bors bot closed this Nov 26, 2023
@mathlib-bors mathlib-bors bot deleted the alexjbest/simprw2 branch November 26, 2023 22:11
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. t-meta Tactics, attributes or user commands

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants