Skip to content

[Merged by Bors] - feat: Add getVert_append and getVert_reverse#11787

Closed
IvanRenison wants to merge 1 commit intomasterfrom
IvanRenison/getVert_append_and_reverse
Closed

[Merged by Bors] - feat: Add getVert_append and getVert_reverse#11787
IvanRenison wants to merge 1 commit intomasterfrom
IvanRenison/getVert_append_and_reverse

Conversation

@IvanRenison
Copy link
Copy Markdown
Collaborator


For using in #9131

Open in Gitpod

@IvanRenison IvanRenison added new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! awaiting-review t-combinatorics Combinatorics labels Mar 30, 2024
Copy link
Copy Markdown
Contributor

@Ruben-VandeVelde Ruben-VandeVelde left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Sorry for the delay. This seems sensible enough to me.

maintainer merge

@github-actions
Copy link
Copy Markdown

🚀 Pull request has been placed on the maintainer queue by Ruben-VandeVelde.

@github-actions github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Apr 18, 2024
@github-actions
Copy link
Copy Markdown

🚀 Pull request has been placed on the maintainer queue by Ruben-VandeVelde.

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

@ghost ghost added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Apr 18, 2024
mathlib-bors bot pushed a commit that referenced this pull request Apr 18, 2024
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Apr 18, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat: Add getVert_append and getVert_reverse [Merged by Bors] - feat: Add getVert_append and getVert_reverse Apr 18, 2024
@mathlib-bors mathlib-bors bot closed this Apr 18, 2024
@mathlib-bors mathlib-bors bot deleted the IvanRenison/getVert_append_and_reverse branch April 18, 2024 09:26
uniwuni pushed a commit that referenced this pull request Apr 19, 2024
callesonne pushed a commit that referenced this pull request Apr 22, 2024
Jun2M pushed a commit that referenced this pull request Apr 24, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! ready-to-merge This PR has been sent to bors. t-combinatorics Combinatorics

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants