Skip to content

[Merged by Bors] - chore: update std 05-22#4248

Closed
digama0 wants to merge 7 commits intomasterfrom
bump-05-22
Closed

[Merged by Bors] - chore: update std 05-22#4248
digama0 wants to merge 7 commits intomasterfrom
bump-05-22

Conversation

@digama0
Copy link
Copy Markdown
Member

@digama0 digama0 commented May 23, 2023

The main breaking change is that tac <;> [t1, t2] is now written tac <;> [t1; t2], to avoid clashing with tactics like cases and use that take comma-separated lists.


Open in Gitpod

@fpvandoorn
Copy link
Copy Markdown
Member

Thanks!

bors merge

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels May 23, 2023
bors bot pushed a commit that referenced this pull request May 23, 2023
The main breaking change is that `tac <;> [t1, t2]` is now written `tac <;> [t1; t2]`, to avoid clashing with tactics like `cases` and `use` that take comma-separated lists.
@bors
Copy link
Copy Markdown

bors bot commented May 24, 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: update std 05-22 [Merged by Bors] - chore: update std 05-22 May 24, 2023
@bors bors bot closed this May 24, 2023
@bors bors bot deleted the bump-05-22 branch May 24, 2023 01:45
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.

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants