Skip to content

[Merged by Bors] - chore: fix SHA in Data.Buffer.Basic#5894

Closed
eric-wieser wants to merge 3 commits intomasterfrom
fix-buffer-sha
Closed

[Merged by Bors] - chore: fix SHA in Data.Buffer.Basic#5894
eric-wieser wants to merge 3 commits intomasterfrom
fix-buffer-sha

Conversation

@eric-wieser
Copy link
Copy Markdown
Member

Also adds noaligns


Open in Gitpod

@eric-wieser eric-wieser added awaiting-review mathlib3-pair This PR is a forward-port of a mathlib3 PR or part of one, either under review or recently merged labels Jul 14, 2023
@eric-wieser eric-wieser changed the title chore: fix SHA in Data.Buffer.Parser chore: fix SHA in Data.Buffer.Basic Jul 14, 2023
@eric-wieser eric-wieser added the easy < 20s of review time. See the lifecycle page for guidelines. label Jul 14, 2023
@kim-em
Copy link
Copy Markdown
Contributor

kim-em commented Jul 16, 2023

bors merge

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Jul 16, 2023
bors bot pushed a commit that referenced this pull request Jul 16, 2023
@bors
Copy link
Copy Markdown

bors bot commented Jul 16, 2023

This PR was included in a batch that was canceled, it will be automatically retried

bors bot pushed a commit that referenced this pull request Jul 16, 2023
@bors
Copy link
Copy Markdown

bors bot commented Jul 16, 2023

This PR was included in a batch that was canceled, it will be automatically retried

bors bot pushed a commit that referenced this pull request Jul 16, 2023
@bors
Copy link
Copy Markdown

bors bot commented Jul 16, 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 SHA in Data.Buffer.Basic [Merged by Bors] - chore: fix SHA in Data.Buffer.Basic Jul 16, 2023
@bors bors bot closed this Jul 16, 2023
@bors bors bot deleted the fix-buffer-sha branch July 16, 2023 13:05
kim-em pushed a commit that referenced this pull request Aug 14, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

easy < 20s of review time. See the lifecycle page for guidelines. mathlib3-pair This PR is a forward-port of a mathlib3 PR or part of one, either under review or recently merged 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