Skip to content

[Merged by Bors] - feat: Try this: for multiple rewrites#6434

Closed
kim-em wants to merge 3 commits intomasterfrom
try_this_rws
Closed

[Merged by Bors] - feat: Try this: for multiple rewrites#6434
kim-em wants to merge 3 commits intomasterfrom
try_this_rws

Conversation

@kim-em
Copy link
Copy Markdown
Contributor

@kim-em kim-em commented Aug 8, 2023

Splitting this off from #6120, hopefully for faster review.

I would like to upstream this file to Std, as it it used by exact?.

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 Aug 8, 2023
@kim-em kim-em mentioned this pull request Aug 8, 2023
Closed
11 tasks
@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 8, 2023
@alexjbest
Copy link
Copy Markdown
Member

alexjbest commented Aug 8, 2023

maintainer merge

@github-actions
Copy link
Copy Markdown

github-actions bot commented Aug 8, 2023

🚀 Pull request has been placed on the maintainer queue by alexjbest.

@j-loreaux
Copy link
Copy Markdown
Contributor

j-loreaux commented Aug 8, 2023

I don't want to slow this down unnecessarily, but should this have associated tests? Or is that just stupid?

@alexjbest
Copy link
Copy Markdown
Member

alexjbest commented Aug 8, 2023

I don't think its stupid! And it may even be a reasonable request. That the old behaviour still works is implicitly tested in the rewrites tests file. And I assume that when rewrite search lands tests will come. It also seems slightly hard for something to work for lists of length one and fail for longer ones, though that is of course possible.

@j-loreaux
Copy link
Copy Markdown
Contributor

j-loreaux commented Aug 8, 2023

bors r+

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Aug 8, 2023
bors bot pushed a commit that referenced this pull request Aug 8, 2023
@kim-em
feat: Try this: for multiple rewrites (#6434)
730a984 
Splitting this off from #6120, hopefully for faster review.

I would like to upstream this file to Std, as it it used by `exact?`.



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

bors bot commented Aug 8, 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 feat: Try this: for multiple rewrites [Merged by Bors] - feat: Try this: for multiple rewrites Aug 8, 2023
@bors bors bot closed this Aug 8, 2023
@bors bors bot deleted the try_this_rws branch August 8, 2023 19:28
kim-em added a commit that referenced this pull request Aug 14, 2023
@kim-em
feat: Try this: for multiple rewrites (#6434)
fe8bb9d 
Splitting this off from #6120, hopefully for faster review.

I would like to upstream this file to Std, as it it used by `exact?`.



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

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 @alexjbest @j-loreaux