Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

[Merged by Bors] - fix(scripts/add_port_comments): do not insert extra blank lines#17850

Closed
eric-wieser wants to merge 1 commit intomasterfrom
eric-wieser/fix-port-comment-whitespace
Closed

[Merged by Bors] - fix(scripts/add_port_comments): do not insert extra blank lines#17850
eric-wieser wants to merge 1 commit intomasterfrom
eric-wieser/fix-port-comment-whitespace

Conversation

@eric-wieser
Copy link
Copy Markdown
Member

@eric-wieser eric-wieser commented Dec 8, 2022

Since we insert the comment with a trailing newline, we should remove an extra newline when removing it.


Open in Gitpod

@eric-wieser eric-wieser added easy < 20s of review time. See the lifecycle page for guidelines. awaiting-review The author would like community review of the PR labels Dec 8, 2022
@eric-wieser eric-wieser requested a review from jcommelin December 8, 2022 00:39
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

@leanprover-community-bot-assistant leanprover-community-bot-assistant added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Dec 8, 2022
bors bot pushed a commit that referenced this pull request Dec 8, 2022
Since we insert the comment with a trailing newline, we should remove an extra newline when removing it.
@bors
Copy link
Copy Markdown

bors bot commented Dec 8, 2022

Build failed (retrying...):

bors bot pushed a commit that referenced this pull request Dec 8, 2022
Since we insert the comment with a trailing newline, we should remove an extra newline when removing it.
@bors
Copy link
Copy Markdown

bors bot commented Dec 8, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title fix(scripts/add_port_comments): do not insert extra blank lines [Merged by Bors] - fix(scripts/add_port_comments): do not insert extra blank lines Dec 8, 2022
@bors bors bot closed this Dec 8, 2022
@bors bors bot deleted the eric-wieser/fix-port-comment-whitespace branch December 8, 2022 15:37
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.

Labels

easy < 20s of review time. See the lifecycle page for guidelines. ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.)

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants