Skip to content

[Merged by Bors] - chore(*): drop $/<| before fun#9361

Closed
urkud wants to merge 1 commit intomasterfrom
YK-dollar-fun
Closed

[Merged by Bors] - chore(*): drop $/<| before fun#9361
urkud wants to merge 1 commit intomasterfrom
YK-dollar-fun

Conversation

@urkud
Copy link
Copy Markdown
Member

@urkud urkud commented Dec 30, 2023

Subset of #9319

Open in Gitpod

@urkud urkud added awaiting-review awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. labels Dec 30, 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 Dec 30, 2023
@digama0
Copy link
Copy Markdown
Member

digama0 commented Dec 30, 2023

bors r+

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Dec 30, 2023
mathlib-bors bot pushed a commit that referenced this pull request Dec 30, 2023
@urkud
chore(*): drop $/<| before fun (#9361)
3694e27 
Subset of #9319
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Dec 30, 2023

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title chore(*): drop $/<| before fun [Merged by Bors] - chore(*): drop $/<| before fun Dec 30, 2023
@mathlib-bors mathlib-bors bot closed this Dec 30, 2023
@mathlib-bors mathlib-bors bot deleted the YK-dollar-fun branch December 30, 2023 23:00
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.

2 participants

@urkud @digama0