Skip to content

[Merged by Bors] - doc: move comments#3666

Closed
chabulhwi wants to merge 1 commit intomasterfrom
move_comments
Closed

[Merged by Bors] - doc: move comments#3666
chabulhwi wants to merge 1 commit intomasterfrom
move_comments

Conversation

@chabulhwi
Copy link
Copy Markdown
Collaborator

Two comments were in the wrong places.


Open in Gitpod

Two comments were in the wrong places.
@chabulhwi chabulhwi added documentation Improvements or additions to documentation awaiting-review labels Apr 27, 2023
@chabulhwi chabulhwi self-assigned this Apr 27, 2023
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 Apr 27, 2023
bors bot pushed a commit that referenced this pull request Apr 27, 2023
Two comments were in the wrong places.
@bors
Copy link
Copy Markdown

bors bot commented Apr 27, 2023

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title doc: move comments [Merged by Bors] - doc: move comments Apr 27, 2023
@bors bors bot closed this Apr 27, 2023
@bors bors bot deleted the move_comments branch April 27, 2023 08:41
kim-em pushed a commit that referenced this pull request May 10, 2023
Two comments were in the wrong places.
hrmacbeth pushed a commit that referenced this pull request May 10, 2023
Two comments were in the wrong places.
hrmacbeth pushed a commit that referenced this pull request May 11, 2023
Two comments were in the wrong places.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

documentation Improvements or additions to documentation ready-to-merge This PR has been sent to bors.

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants