Skip to content

[Merged by Bors] - chore: empty port of the Data.Buffer.Parser in core#5864

Closed
Komyyy wants to merge 5 commits intomasterfrom
port/Data.Buffer.Parser
Closed

[Merged by Bors] - chore: empty port of the Data.Buffer.Parser in core#5864
Komyyy wants to merge 5 commits intomasterfrom
port/Data.Buffer.Parser

Conversation

@Komyyy
Copy link
Copy Markdown
Contributor

@Komyyy Komyyy commented Jul 13, 2023

addition to #5848

Open in Gitpod

@Komyyy Komyyy added awaiting-review mathlib-port This is a port of a theory file from mathlib. easy < 20s of review time. See the lifecycle page for guidelines. awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. labels Jul 13, 2023
jcommelin
jcommelin reviewed Jul 13, 2023
View reviewed changes
@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 Jul 13, 2023
@Komyyy Komyyy added the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Jul 13, 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 Jul 13, 2023
@Komyyy Komyyy added awaiting-review awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. labels Jul 13, 2023
jcommelin
jcommelin reviewed Jul 13, 2023
View reviewed changes
jcommelin
jcommelin approved these changes Jul 13, 2023
View reviewed changes
Copy link
Copy Markdown
Member

@jcommelin jcommelin 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 merge

@kim-em kim-em added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Jul 13, 2023
bors bot pushed a commit that referenced this pull request Jul 13, 2023
@Komyyy
chore: empty port of the Data.Buffer.Parser in core (#5864)
4d8f5b5 
addition to #5848
@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 Jul 13, 2023
@bors
Copy link
Copy Markdown

bors bot commented Jul 13, 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: empty port of the Data.Buffer.Parser in core [Merged by Bors] - chore: empty port of the Data.Buffer.Parser in core Jul 13, 2023
@bors bors bot closed this Jul 13, 2023
@bors bors bot deleted the port/Data.Buffer.Parser branch July 13, 2023 15:42
kim-em pushed a commit that referenced this pull request Aug 14, 2023
@Komyyy @kim-em
chore: empty port of the Data.Buffer.Parser in core (#5864)
f5ac30d 
addition to #5848
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@jcommelin jcommelin jcommelin approved these changes

Assignees

No one assigned

Labels

easy < 20s of review time. See the lifecycle page for guidelines. mathlib-port This is a port of a theory file from mathlib. 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

@Komyyy @jcommelin @kim-em