Skip to content

[Merged by Bors] - chore: fix nonterminal simps#7497

Closed
BoltonBailey wants to merge 7 commits intomasterfrom
BoltonBailey/nonterminal-simp-removal-squad
Closed

[Merged by Bors] - chore: fix nonterminal simps#7497
BoltonBailey wants to merge 7 commits intomasterfrom
BoltonBailey/nonterminal-simp-removal-squad

Conversation

@BoltonBailey
Copy link
Copy Markdown
Collaborator

@BoltonBailey BoltonBailey commented Oct 4, 2023

Fixes the nonterminal simps identified by #7496

Open in Gitpod

@BoltonBailey BoltonBailey added the WIP Work in progress label Oct 4, 2023
@BoltonBailey BoltonBailey mentioned this pull request Oct 4, 2023
Closed
3 tasks
@BoltonBailey BoltonBailey added awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. and removed WIP Work in progress labels Oct 4, 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 Oct 4, 2023
ocfnash
ocfnash approved these changes Oct 5, 2023
View reviewed changes
Copy link
Copy Markdown
Contributor

@ocfnash ocfnash left a comment

Choose a reason for hiding this comment

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

Thanks!

bors d+

@bors
Copy link
Copy Markdown

bors bot commented Oct 5, 2023

✌️ BoltonBailey 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 Oct 5, 2023
@BoltonBailey
Copy link
Copy Markdown
Collaborator Author

BoltonBailey commented Oct 5, 2023

bors r+

bors bot pushed a commit that referenced this pull request Oct 5, 2023
@BoltonBailey
chore: fix nonterminal simps (#7497)
19ca95b 
Fixes the nonterminal simps identified by #7496
@bors
Copy link
Copy Markdown

bors bot commented Oct 5, 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: fix nonterminal simps [Merged by Bors] - chore: fix nonterminal simps Oct 5, 2023
@bors bors bot closed this Oct 5, 2023
@bors bors bot deleted the BoltonBailey/nonterminal-simp-removal-squad branch October 5, 2023 21:20
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@ocfnash ocfnash ocfnash approved these changes

Assignees

No one assigned

Labels

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

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@BoltonBailey @ocfnash